diff -r fd510875fb71 -r d12da312eff4 src/FOLP/ROOT.ML
--- a/src/FOLP/ROOT.ML	Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/ROOT.ML	Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	FOLP/ROOT
+(*  Title:      FOLP/ROOT
     ID:         $Id$
-    Author: 	martin Coen, Cambridge University Computer Laboratory
+    Author:     martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Modifed version of Lawrence Paulson's FOL that contains proof terms.
@@ -20,7 +20,7 @@
 
 use "hypsubst.ML";
 use "classical.ML";      (* Patched 'cos matching won't instantiate proof *)
-use "simp.ML";	         (* Patched 'cos matching won't instantiate proof *)
+use "simp.ML";           (* Patched 'cos matching won't instantiate proof *)
 
 
 (*** Applying HypsubstFun to generate hyp_subst_tac ***)
@@ -34,7 +34,7 @@
 
   (*etac rev_cut_eq moves an equality to be the last premise. *)
   val rev_cut_eq = prove_goal IFOLP.thy 
-		"[| p:a=b;  !!x.x:a=b ==> f(x):R |] ==> ?p:R"
+                "[| p:a=b;  !!x.x:a=b ==> f(x):R |] ==> ?p:R"
    (fn prems => [ REPEAT(resolve_tac prems 1) ]);
 
   val rev_mp = rev_mp
@@ -78,4 +78,4 @@
 use "../Pure/install_pp.ML";
 print_depth 8;
 
-val FOLP_build_completed = ();	(*indicate successful build*)
+val FOLP_build_completed = ();  (*indicate successful build*)