src/Provers/classical.ML
changeset 32960 69916a850301
parent 32952 aeb1e44fbc19
child 33317 b4534348b8fd
     1.1 --- a/src/Provers/classical.ML	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/Provers/classical.ML	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -363,7 +363,7 @@
     1.4      (warning ("Ignoring duplicate safe elimination (elim!)\n" ^
     1.5          Display.string_of_thm_without_context th); cs)
     1.6    else if has_fewer_prems 1 th then
     1.7 -    	error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
     1.8 +        error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
     1.9    else
    1.10    let
    1.11        val th' = classical_rule (flat_rule th)
    1.12 @@ -390,7 +390,7 @@
    1.13  
    1.14  fun make_elim th =
    1.15      if has_fewer_prems 1 th then
    1.16 -    	  error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
    1.17 +          error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
    1.18      else Tactic.make_elim th;
    1.19  
    1.20  fun cs addSDs ths = cs addSEs (map make_elim ths);
    1.21 @@ -431,7 +431,7 @@
    1.22      (warning ("Ignoring duplicate elimination (elim)\n" ^
    1.23          Display.string_of_thm_without_context th); cs)
    1.24    else if has_fewer_prems 1 th then
    1.25 -    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
    1.26 +        error("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
    1.27    else
    1.28    let
    1.29        val th' = classical_rule (flat_rule th)