diff -r fd510875fb71 -r d12da312eff4 src/FOLP/hypsubst.ML
--- a/src/FOLP/hypsubst.ML	Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/hypsubst.ML	Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	FOLP/hypsubst
+(*  Title:      FOLP/hypsubst
     ID:         $Id$
-    Author: 	Martin D Coen, Cambridge University Computer Laboratory
+    Author:     Martin D Coen, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
 Original version of Provers/hypsubst.  Cannot use new version because it
@@ -11,11 +11,11 @@
 
 signature HYPSUBST_DATA =
   sig
-  val dest_eq	: term -> term*term
-  val imp_intr	: thm		(* (P ==> Q) ==> P-->Q *)
-  val rev_mp	: thm		(* [| P;  P-->Q |] ==> Q *)
-  val subst	: thm		(* [| a=b;  P(a) |] ==> P(b) *)
-  val sym	: thm		(* a=b ==> b=a *)
+  val dest_eq   : term -> term*term
+  val imp_intr  : thm           (* (P ==> Q) ==> P-->Q *)
+  val rev_mp    : thm           (* [| P;  P-->Q |] ==> Q *)
+  val subst     : thm           (* [| a=b;  P(a) |] ==> P(b) *)
+  val sym       : thm           (* a=b ==> b=a *)
   end;
 
 signature HYPSUBST =
@@ -44,13 +44,13 @@
 fun inspect_pair bnd (t,u) =
   case (Pattern.eta_contract t, Pattern.eta_contract u) of
        (Bound i, _) => if loose(i,u) then raise Match 
-		       else sym		(*eliminates t*)
+                       else sym         (*eliminates t*)
      | (_, Bound i) => if loose(i,t) then raise Match 
-		       else asm_rl	(*eliminates u*)
+                       else asm_rl      (*eliminates u*)
      | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match 
-		      else sym		(*eliminates t*)
+                      else sym          (*eliminates t*)
      | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match 
-		      else asm_rl	(*eliminates u*)
+                      else asm_rl       (*eliminates u*)
      | _ => raise Match;
 
 (*Locates a substitutable variable on the left (resp. right) of an equality
@@ -58,25 +58,25 @@
    the rule asm_rl (resp. sym). *)
 fun eq_var bnd =
   let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
-	| eq_var_aux k (Const("==>",_) $ A $ B) = 
-	      ((k, inspect_pair bnd (dest_eq A))
-		      (*Exception Match comes from inspect_pair or dest_eq*)
-	       handle Match => eq_var_aux (k+1) B)
-	| eq_var_aux k _ = raise EQ_VAR
+        | eq_var_aux k (Const("==>",_) $ A $ B) = 
+              ((k, inspect_pair bnd (dest_eq A))
+                      (*Exception Match comes from inspect_pair or dest_eq*)
+               handle Match => eq_var_aux (k+1) B)
+        | eq_var_aux k _ = raise EQ_VAR
   in  eq_var_aux 0  end;
 
 (*Select a suitable equality assumption and substitute throughout the subgoal
   Replaces only Bound variables if bnd is true*)
 fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
       let val (_,_,Bi,_) = dest_state(state,i)
-	  val n = length(Logic.strip_assums_hyp Bi) - 1
-	  val (k,symopt) = eq_var bnd Bi
+          val n = length(Logic.strip_assums_hyp Bi) - 1
+          val (k,symopt) = eq_var bnd Bi
       in 
-	 EVERY [REPEAT_DETERM_N k (etac rev_mp i),
-		etac revcut_rl i,
-		REPEAT_DETERM_N (n-k) (etac rev_mp i),
-		etac (symopt RS subst) i,
-		REPEAT_DETERM_N n (rtac imp_intr i)]
+         EVERY [REPEAT_DETERM_N k (etac rev_mp i),
+                etac revcut_rl i,
+                REPEAT_DETERM_N (n-k) (etac rev_mp i),
+                etac (symopt RS subst) i,
+                REPEAT_DETERM_N n (rtac imp_intr i)]
       end
       handle THM _ => no_tac | EQ_VAR => no_tac));