src/Provers/classical.ML
changeset 32960 69916a850301
parent 32952 aeb1e44fbc19
child 33317 b4534348b8fd
--- a/src/Provers/classical.ML	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/Provers/classical.ML	Sat Oct 17 14:43:18 2009 +0200
@@ -363,7 +363,7 @@
     (warning ("Ignoring duplicate safe elimination (elim!)\n" ^
         Display.string_of_thm_without_context th); cs)
   else if has_fewer_prems 1 th then
-    	error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
+        error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
   else
   let
       val th' = classical_rule (flat_rule th)
@@ -390,7 +390,7 @@
 
 fun make_elim th =
     if has_fewer_prems 1 th then
-    	  error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
+          error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
     else Tactic.make_elim th;
 
 fun cs addSDs ths = cs addSEs (map make_elim ths);
@@ -431,7 +431,7 @@
     (warning ("Ignoring duplicate elimination (elim)\n" ^
         Display.string_of_thm_without_context th); cs)
   else if has_fewer_prems 1 th then
-    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
+        error("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
   else
   let
       val th' = classical_rule (flat_rule th)