src/HOL/Tools/res_reconstruct.ML

       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: " ^ Toplevel.exn_message e
+    let val msg = "Translation of TSTP raised an exception: " ^ ML_Compiler.exn_message e
     in  trace msg; msg  end;
 
 
     
   (* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)