src/Pure/IsaPlanner/term_lib.ML
changeset 17931 881274f283cf
parent 17797 9996f3a0ffdf
child 18036 d5d5ad4b78c5
equal deleted inserted replaced
17930:e7160d70be1f 17931:881274f283cf
   247 fun term_of_thm t = (Thm.prop_of t);
   247 fun term_of_thm t = (Thm.prop_of t);
   248 
   248 
   249 fun string_of_term t = Sign.string_of_term (the_context()) t;
   249 fun string_of_term t = Sign.string_of_term (the_context()) t;
   250 fun print_term t = writeln (string_of_term t);
   250 fun print_term t = writeln (string_of_term t);
   251 
   251 
   252 (* create a trivial HOL thm from anything... *)
   252 (* create a trivial thm from anything... *)
   253 fun triv_thm_from_string s = Thm.trivial (cterm_of (the_context()) (read s));
   253 fun triv_thm_from_string s =
       
   254   let val thy = the_context()
       
   255   in Thm.trivial (cterm_of thy (Sign.read_prop thy s)) end;
   254 
   256 
   255   (* Checks if vars could be the same - alpha convertable
   257   (* Checks if vars could be the same - alpha convertable
   256   w.r.t. previous vars, a and b are assumed to be vars,
   258   w.r.t. previous vars, a and b are assumed to be vars,
   257   free vars, but not bound vars,
   259   free vars, but not bound vars,
   258   Note frees and vars must all have unique names. *)
   260   Note frees and vars must all have unique names. *)