more antiquotations instead of adhoc ML stuff;
authorwenzelm
Fri Jul 24 22:59:08 2009 +0200 (2009-07-24)
changeset 321817e460c2d4223
parent 32180 37800cb1d378
child 32182 f01207d56583
more antiquotations instead of adhoc ML stuff;
src/HOL/Tools/inductive.ML
     1.1 --- a/src/HOL/Tools/inductive.ML	Fri Jul 24 22:31:27 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Fri Jul 24 22:59:08 2009 +0200
     1.3 @@ -96,11 +96,12 @@
     1.4  
     1.5  val notTrueE = TrueI RSN (2, notE);
     1.6  val notFalseI = Seq.hd (atac 1 notI);
     1.7 -val simp_thms' = map (fn s => mk_meta_eq (the (find_first
     1.8 -  (equal (OldGoals.read_prop @{theory HOL} s) o prop_of) simp_thms)))
     1.9 -  ["(~True) = False", "(~False) = True",
    1.10 -   "(True --> ?P) = ?P", "(False --> ?P) = True",
    1.11 -   "(?P & True) = ?P", "(True & ?P) = ?P"];
    1.12 +
    1.13 +val simp_thms' = map mk_meta_eq
    1.14 +  @{lemma "(~True) = False" "(~False) = True"
    1.15 +      "(True --> P) = P" "(False --> P) = True"
    1.16 +      "(P & True) = P" "(True & P) = P"
    1.17 +    by (fact simp_thms)+};
    1.18  
    1.19  
    1.20