changeset 50668 | e25275f7d15e |
parent 50557 | 31313171deb5 |
child 50669 | 84c7cf36b2e0 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jan 02 09:42:57 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jan 02 10:41:53 2013 +0100 @@ -95,7 +95,7 @@ |> Output.urgent_message fun really_go () = problem - |> get_minimizing_prover ctxt mode learn name params minimize_command + |> get_minimizing_isar_prover ctxt mode learn name params minimize_command |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, ...} => print_used_facts used_facts | _ => ())