changeset 56303 | 4cc3f4db3447 |
parent 56254 | a2dd9200854d |
child 56995 | 61855ade6c7e |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Mar 27 13:00:40 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Mar 27 17:12:40 2014 +0100 @@ -337,7 +337,7 @@ else (trace_msg ctxt (fn () => "Internal error when " ^ when ^ ":\n" ^ - ML_Compiler.exn_message exn); def) + Runtime.exn_message exn); def) fun graph_info G = string_of_int (length (Graph.keys G)) ^ " node(s), " ^