author | wenzelm |
Sat, 06 Jun 2009 21:46:36 +0200 | |
changeset 31479 | 08e2a70d002a |
parent 31478 | 5e412e4c6546 |
child 31480 | 05937d6aafb5 |
--- a/src/HOL/Tools/res_reconstruct.ML Sat Jun 06 21:11:23 2009 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Sat Jun 06 21:46:36 2009 +0200 @@ -452,7 +452,7 @@ 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;