ResAxioms.neg_conjecture_clauses: proper context;
let exceptions get through unhindered -- Poly/ML exception_trace will do the tracing;

--- a/src/HOL/Tools/res_reconstruct.ML	Tue Jul 28 18:17:35 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Tue Jul 28 18:17:36 2009 +0200
@@ -442,7 +442,7 @@
       val _ = trace (Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
       val (_,lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
       val _ = trace (Int.toString (length lines) ^ " lines extracted\n")
-      val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
+      val (ccls,fixes) = ResAxioms.neg_conjecture_clauses ctxt th sgno
       val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
       val ccls = map forall_intr_vars ccls
       val _ =
@@ -452,10 +452,7 @@
       val _ = trace "\ndecode_tstp_file: finishing\n"
   in
     isar_header (map #1 fixes) ^ String.concat ilines ^ "qed\n"
-  end
-  handle e => (*FIXME: exn handler is too general!*)
-    let val msg = "Translation of TSTP raised an exception: " ^ ML_Compiler.exn_message e
-    in  trace msg; msg  end;
+  end;
 
 
   (*=== EXTRACTING PROOF-TEXT === *)