changeset 38290 | 581a402a80f0 |
parent 38282 | 319c59682c51 |
child 38455 | 131f7c46cf2c |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 09 14:00:32 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 09 14:08:30 2010 +0200 @@ -363,6 +363,8 @@ in prover params (minimize_command name) problem |> #message handle ERROR message => "Error: " ^ message ^ "\n" + | exn => "Internal error: \n" ^ ML_Compiler.exn_message exn ^ + "\n" end) end