Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
OldGoals.read_prop;
authorwenzelm
Wed, 18 Jun 2008 18:55:00 +0200
changeset 27252 042aebff17e1
parent 27251 121991a4884d
child 27253 ffbe8b4ebd22
OldGoals.read_prop;
src/HOL/Tools/inductive_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/inductive_package.ML	Wed Jun 18 18:54:59 2008 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Wed Jun 18 18:55:00 2008 +0200
@@ -97,7 +97,7 @@
 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 (Sign.read_prop HOL.thy s) o prop_of) simp_thms)))
+  (equal (OldGoals.read_prop HOL.thy s) o prop_of) simp_thms)))
   ["(~True) = False", "(~False) = True",
    "(True --> ?P) = ?P", "(False --> ?P) = True",
    "(?P & True) = ?P", "(True & ?P) = ?P"];
isabelle