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))