diff -r e7160d70be1f -r 881274f283cf src/Pure/IsaPlanner/term_lib.ML
--- 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,