src/HOL/Tools/Sledgehammer/sledgehammer.ML
changeset 38290 581a402a80f0
parent 38282 319c59682c51
child 38455 131f7c46cf2c
equal deleted inserted replaced
38289:74dd8dd33512 38290:581a402a80f0
   361                 {subgoal = i, goal = (ctxt, (facts, goal)),
   361                 {subgoal = i, goal = (ctxt, (facts, goal)),
   362                  relevance_override = relevance_override, axioms = NONE}
   362                  relevance_override = relevance_override, axioms = NONE}
   363             in
   363             in
   364               prover params (minimize_command name) problem |> #message
   364               prover params (minimize_command name) problem |> #message
   365               handle ERROR message => "Error: " ^ message ^ "\n"
   365               handle ERROR message => "Error: " ^ message ^ "\n"
       
   366                    | exn => "Internal error: \n" ^ ML_Compiler.exn_message exn ^
       
   367                             "\n"
   366             end)
   368             end)
   367   end
   369   end
   368 
   370 
   369 fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set."
   371 fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set."
   370   | run_sledgehammer (params as {atps, ...}) i relevance_override
   372   | run_sledgehammer (params as {atps, ...}) i relevance_override