diff -r fd510875fb71 -r d12da312eff4 src/FOLP/intprover.ML
--- a/src/FOLP/intprover.ML	Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOLP/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
@@ -54,10 +54,10 @@
 
 (*Attack subgoals using safe inferences*)
 val safe_step_tac = FIRST' [uniq_assume_tac,
-			    IFOLP_Lemmas.uniq_mp_tac,
-			    biresolve_tac safe0_brls,
-			    hyp_subst_tac,
-			    biresolve_tac safep_brls] ;
+                            IFOLP_Lemmas.uniq_mp_tac,
+                            biresolve_tac safe0_brls,
+                            hyp_subst_tac,
+                            biresolve_tac safep_brls] ;
 
 (*Repeatedly attack subgoals using safe inferences*)
 val safe_tac = DETERM (REPEAT_FIRST safe_step_tac);