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