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.
avoid lagacy read function;
authorwenzelm
Wed, 19 Oct 2005 21:52:44 +0200
changeset 17931 881274f283cf
parent 17930 e7160d70be1f
child 17932 677f7bec354e
avoid lagacy read function;
src/Pure/IsaPlanner/term_lib.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/IsaPlanner/term_lib.ML	Wed Oct 19 21:52:43 2005 +0200
+++ b/src/Pure/IsaPlanner/term_lib.ML	Wed Oct 19 21:52:44 2005 +0200
@@ -249,8 +249,10 @@
 fun string_of_term t = Sign.string_of_term (the_context()) t;
 fun print_term t = writeln (string_of_term t);
 
-(* create a trivial HOL thm from anything... *)
-fun triv_thm_from_string s = Thm.trivial (cterm_of (the_context()) (read s));
+(* create a trivial thm from anything... *)
+fun triv_thm_from_string s =
+  let val thy = the_context()
+  in Thm.trivial (cterm_of thy (Sign.read_prop thy s)) end;
 
   (* Checks if vars could be the same - alpha convertable
   w.r.t. previous vars, a and b are assumed to be vars,
isabelle