diff -urP OpenProofPower-2.8.1p1/patches/patch-2.8.1.rda.091011.txt OpenProofPower-2.8.1p1.rda.091011/patches/patch-2.8.1.rda.091011.txt
--- OpenProofPower-2.8.1p1/patches/patch-2.8.1.rda.091011.txt	1970-01-01 01:00:00.000000000 +0100
+++ OpenProofPower-2.8.1p1.rda.091011/patches/patch-2.8.1.rda.091011.txt	2009-10-11 14:08:42.000000000 +0100
@@ -0,0 +1,19 @@
+
+Date: 11th October 2009
+Source: Rob Arthan rda@lemma-one.com
+Purpose: Speed up performance under Poly/ML version 5.3
+Description:
+From version 5.3 of Poly/ML, abstype values are pretty-printed in full
+rather than as "?". This has a performance impact on some ProofPower
+functions such as pp_make_database. This patch suppresses pretty-printing
+for the type that was causing the problem.
+
+        cd $HOME/bld/OpenProofPower-2.8.1
+        gunzip -c /tmp/patch-2.8.1.rda.091011.gz | patch -p1 -b -B orig/
+
+Then follow the usual instructions for installation in the README file.
+
+Alternatively a version of the source is supplied on the ProofPower
+website with all recommended patches applied. Currently this is:
+
+http://www.lemma-one.com/ProofPower/getting/versions/OpenProofPower-2.8.1p2.tgz
diff -urP OpenProofPower-2.8.1p1/src/imp025.doc OpenProofPower-2.8.1p1.rda.091011/src/imp025.doc
--- OpenProofPower-2.8.1p1/src/imp025.doc	2009-09-09 17:40:38.000000000 +0100
+++ OpenProofPower-2.8.1p1.rda.091011/src/imp025.doc	2009-10-11 14:00:41.000000000 +0100
@@ -8,18 +8,18 @@
 
 Contact: Rob Arthan < rda@lemma-one.com >
 ********************************************************************************
-% imp025.doc   %Z% 2006/01/16 17:47:20 2.15 imp025.doc,v
+% imp025.doc   %Z% $Date: 2009/09/14 14:56:56 $ $Revision: 2.16 $ $RCSfile: imp025.doc,v $
 
 =TEX
-% imp025.doc   %Z% 2006/01/16 17:47:20 2.15 imp025.doc,v
+% imp025.doc   %Z% $Date: 2009/09/14 14:56:56 $ $Revision: 2.16 $ $RCSfile: imp025.doc,v $
 \documentstyle[hol1,11pt,TQ]{article}
 
 \TPPtitle{Implementation of Pretty Printer}
 \TPPref{DS/FMU/IED/IMP025}
-\def\SCCSissue{2.15%
+\def\SCCSissue{$Revision: 2.16 $%
 }
 \TPPissue{\SCCSissue}
-\TPPdate{\FormatDate{2006/01/16 17:47:20%
+\TPPdate{\FormatDate{$Date: 2009/09/14 14:56:56 $%
 }}
 \TPPproject{FST PROJECT}
 
@@ -123,6 +123,7 @@
 \item[Issue 2.13] PPHol-specific updates for open source release
 \item[Issue 2.14] The prefix for private interfaces is now $pp'$ rather than $icl'$.
 \item[Issue 2.15] {\em show\_theorem} renamed as {\em show\_thm}.
+\item[Issue 2.16] Now installs a pretty-printer for the theory hierarchy type to avoid overhead of having the data structure printed out when new databases are made.
 \end{description}
 
 %********************************************************************
@@ -390,7 +391,15 @@
 =TEX
 }
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+=SML
+fun Ûshow_hierarchyÝ(_:int OPT)
+			(o_funs as (addstring, _, _, _):OPPEN_FUNS)
+			(_ : pp'Kernel.pp'HIERARCHY) : unit = (
+	addstring "?"
+
+);
+=TEX
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %\newpage
 \section{INSTALLATION}
 
@@ -438,7 +447,13 @@
 =INSTALLPP
 	(PPCompiler.make_pp
 	["pp'Kernel", "THM"]
-	(interpose show_thm "show_thm"))
+	(interpose show_thm "show_thm"));
+=SML
+=INSTALLPP
+	(PPCompiler.make_pp
+	["pp'Kernel", "pp'HIERARCHY"]
+	(interpose show_hierarchy "show_hierarchy"));
+	()
 );
 
 end;