--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Nov 19 18:14:56 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Nov 19 18:34:04 2013 +0100
@@ -368,7 +368,7 @@
val goal = prop_of (#goal (Proof.goal state))
val facts = nearly_all_facts ctxt false fact_override Symtab.empty
Termtab.empty [] [] goal
- fun learn prover = mash_learn_proof ctxt params prover goal facts
+ val learn = mash_learn_proof ctxt params goal facts
in run_minimize params learn i (#add fact_override) state end
else if subcommand = messagesN then
messages opt_i