# HG changeset patch
# User wenzelm
# Date 1322400417 -3600
# Node ID 7654f750fb438d71d056e1646cbe98612d6743e4
# Parent  96af0578571cc960278c4d5750c7f46f27e88931
more antiquotations;

diff -r 96af0578571c -r 7654f750fb43 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sun Nov 27 14:20:31 2011 +0100
+++ b/src/HOL/Tools/inductive.ML	Sun Nov 27 14:26:57 2011 +0100
@@ -99,9 +99,6 @@
 val inductive_rulify = @{thms induct_rulify};
 val inductive_rulify_fallback = @{thms induct_rulify_fallback};
 
-val notTrueE = TrueI RSN (2, notE);
-val notFalseI = Seq.hd (atac 1 notI);
-
 val simp_thms' = map mk_meta_eq
   @{lemma "(~True) = False" "(~False) = True"
       "(True --> P) = P" "(False --> P) = True"
@@ -372,7 +369,7 @@
       (mono RS (fp_def RS
         (if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold})));
 
-    val rules = [refl, TrueI, notFalseI, exI, conjI];
+    val rules = [refl, TrueI, @{lemma "~ False" by (rule notI)}, exI, conjI];
 
     val intrs = map_index (fn (i, intr) =>
       Skip_Proof.prove ctxt [] [] intr (fn _ => EVERY
@@ -403,7 +400,7 @@
     val intrs = map dest_intr intr_ts ~~ intr_names;
 
     val rules1 = [disjE, exE, FalseE];
-    val rules2 = [conjE, FalseE, notTrueE];
+    val rules2 = [conjE, FalseE, @{lemma "~ True ==> R" by (rule notE [OF _ TrueI])}];
 
     fun prove_elim c =
       let