# HG changeset patch
# User paulson
# Date 1189172125 -7200
# Node ID bb7fdd10de9a534f56c0fedcd614e336181c5cee
# Parent  af7ef6bcc149694ddcaad4d8d630b267c947cee6
allow TVars during type inference

diff -r af7ef6bcc149 -r bb7fdd10de9a src/HOL/Tools/res_reconstruct.ML
--- 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))