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.
allow TVars during type inference
authorpaulson
Fri, 07 Sep 2007 15:35:25 +0200
changeset 24552 bb7fdd10de9a
parent 24551 af7ef6bcc149
child 24553 9b19da7b2b08
allow TVars during type inference
src/HOL/Tools/res_reconstruct.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/res_reconstruct.ML	Fri Sep 07 15:34:32 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Fri Sep 07 15:35:25 2007 +0200
@@ -442,6 +442,7 @@
 
 fun decode_tstp_file cnfs ctxt th sgno thm_names =
   let val tuples = map (dest_tstp o tstp_line o explode) cnfs
+      val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
       val nonnull_lines =
               foldr add_nonnull_prfline []
                     (foldr add_prfline [] (decode_tstp_list ctxt tuples))
isabelle