diff -urP OpenProofPower-2.7.6/patches/patch-2.7.6.rda.060622.txt OpenProofPower-2.7.6.rda.060622/patches/patch-2.7.6.rda.060622.txt
--- OpenProofPower-2.7.6/patches/patch-2.7.6.rda.060622.txt	1970-01-01 01:00:00.000000000 +0100
+++ OpenProofPower-2.7.6.rda.060622/patches/patch-2.7.6.rda.060622.txt	2006-06-22 16:22:05.000000000 +0100
@@ -0,0 +1,15 @@
+Date: 22nd June 2006
+Source: Rob Arthan rda@lemma-one.com
+Purpose: Makes ProofPower version 2.7.6 compile under Poly/ML 4.2.0
+Description:
+The PPHol, PPZed and PPDaz packages will not build on Poly/ML 4.2.0.
+That version of Poly/ML is recommended for use on newer Linux releases.
+This patch makes these packages compatible with Poly/ML 4.2.0. Do not
+apply this patch if you are using Poly/ML 4.1.3.
+
+To apply, patch the source as usual, e.g.,:
+
+        cd $HOME/bld/OpenProofPower-2.7.6
+        gunzip -c /tmp/patch-2.7.5.rda.060622.gz | patch -p1 -b -B orig/
+
+Then follow the usual instructions for installation in the README file.
diff -urP OpenProofPower-2.7.6/src/imp001.doc OpenProofPower-2.7.6.rda.060622/src/imp001.doc
--- OpenProofPower-2.7.6/src/imp001.doc	2005-09-22 14:03:15.000000000 +0100
+++ OpenProofPower-2.7.6.rda.060622/src/imp001.doc	2006-06-22 16:23:39.000000000 +0100
@@ -8,6 +8,9 @@
 
 Contact: Rob Arthan < rda@lemma-one.com >
 ********************************************************************************
+
+**** THIS FILE IS PATCHED TO WORK WITH POLY/ML 4.2.0.
+
 =TEX
 \documentstyle[hol1,11pt,TQ]{article}
 \ftlinepenalty=9999
@@ -108,6 +111,7 @@
 \item[Issue 2.39] Added {\tt app}.
 \item[Issue 2.40] Tidy-up to improve some of the string and character handling.
 \item[Issue 2.41, 2.42] Updates for SML/NJ 110.54.
+\item[N/A] THIS FILE IS PATCHED TO WORK WITH POLY/ML 4.2.0.
 \end{description}
 %\subsection{Changes Forecast}
 \section{GENERAL}
@@ -1912,15 +1916,9 @@
 		then	()
 		else	let	val new_sz = new_size cur_sz ind;
 				val new_arr = Array.array(new_sz, Nil : '_a OPT);
-=NJML
 				val _ = Array.copy{
 						src = arr,
 						di = 0, dst = new_arr};
-=POLYML
-				val _ = Array.copy{
-						si = 0, src = arr,
-						di = 0, dst = new_arr, len = NONE};
-=SML
 			in	data := new_arr
 			end
 	end
diff -urP OpenProofPower-2.7.6/src/imp108.doc OpenProofPower-2.7.6.rda.060622/src/imp108.doc
--- OpenProofPower-2.7.6/src/imp108.doc	2005-09-22 14:03:15.000000000 +0100
+++ OpenProofPower-2.7.6.rda.060622/src/imp108.doc	2006-06-22 16:23:17.000000000 +0100
@@ -9,6 +9,9 @@
 Contact: Rob Arthan < rda@lemma-one.com >
 ********************************************************************************
 %  %Z% $Date: 2005/06/29 16:01:11 $ $Revision: 1.25 $ $RCSfile: imp108.doc,v $
+
+**** THIS FILE IS PATCHED TO WORK WITH POLY/ML 4.2.0.
+
 =TEX
 % TQtemplate.tex
 \documentstyle[hol1,11pt,TQ]{article}
@@ -87,6 +90,7 @@
 are defined in the standard and are redefined in {\Product}.
 \item[Issue 1.23] Now sets PolyML.Compiler.printInAlphabeticalOrder false.
 \item[Issue 1.24,1.25] Updates for SML/NJ 110.54.
+\item[N/A] THIS FILE IS PATCHED TO WORK WITH POLY/ML 4.2.0.
 \end{description}
 \subsection{Changes Forecast}
 As determined by experience during the porting process.
@@ -141,9 +145,6 @@
 	open BasicIO;
 	val Ûflush_outÝ : outstream -> unit = TextIO.flushOut;
 	val Ûopen_appendÝ : string -> outstream = TextIO.openAppend;
-=POLYML
-	val Ûinput_lineÝ : instream -> string = TextIO.inputLine;
-=NJML
 	fun input_line (strm : instream) : string = (
 		case TextIO.inputLine strm of
 			SOME s => s