more antiquotations instead of adhoc ML stuff;

--- 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)+};