diff -r fd510875fb71 -r d12da312eff4 src/FOL/intprover.ML
--- a/src/FOL/intprover.ML	Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/intprover.ML	Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	FOL/int-prover
+(*  Title:      FOL/int-prover
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
 A naive prover for intuitionistic logic
@@ -56,10 +56,10 @@
 
 (*Attack subgoals using safe inferences -- matching, not resolution*)
 val safe_step_tac = FIRST' [eq_assume_tac,
-			    eq_mp_tac,
-			    bimatch_tac safe0_brls,
-			    hyp_subst_tac,
-			    bimatch_tac safep_brls] ;
+                            eq_mp_tac,
+                            bimatch_tac safe0_brls,
+                            hyp_subst_tac,
+                            bimatch_tac safep_brls] ;
 
 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
 val safe_tac = REPEAT_DETERM_FIRST safe_step_tac;