OldGoals.read_prop;
authorwenzelm
Wed Jun 18 18:55:00 2008 +0200 (2008-06-18)
changeset 27252042aebff17e1
parent 27251 121991a4884d
child 27253 ffbe8b4ebd22
OldGoals.read_prop;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Jun 18 18:54:59 2008 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Jun 18 18:55:00 2008 +0200
     1.3 @@ -97,7 +97,7 @@
     1.4  val notTrueE = TrueI RSN (2, notE);
     1.5  val notFalseI = Seq.hd (atac 1 notI);
     1.6  val simp_thms' = map (fn s => mk_meta_eq (the (find_first
     1.7 -  (equal (Sign.read_prop HOL.thy s) o prop_of) simp_thms)))
     1.8 +  (equal (OldGoals.read_prop HOL.thy 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"];