# HG changeset patch
# User wenzelm
# Date 1248469148 -7200
# Node ID 7e460c2d4223a05452c62c113340c36c5984711f
# Parent  37800cb1d378d77e2df5d38b61bff07c920e3d12
more antiquotations instead of adhoc ML stuff;

diff -r 37800cb1d378 -r 7e460c2d4223 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Jul 24 22:31:27 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Fri Jul 24 22:59:08 2009 +0200
@@ -96,11 +96,12 @@
 
 val notTrueE = TrueI RSN (2, notE);
 val notFalseI = Seq.hd (atac 1 notI);
-val simp_thms' = map (fn s => mk_meta_eq (the (find_first
-  (equal (OldGoals.read_prop @{theory HOL} s) o prop_of) simp_thms)))
-  ["(~True) = False", "(~False) = True",
-   "(True --> ?P) = ?P", "(False --> ?P) = True",
-   "(?P & True) = ?P", "(True & ?P) = ?P"];
+
+val simp_thms' = map mk_meta_eq
+  @{lemma "(~True) = False" "(~False) = True"
+      "(True --> P) = P" "(False --> P) = True"
+      "(P & True) = P" "(True & P) = P"
+    by (fact simp_thms)+};