1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -381,8 +381,8 @@
     1.4          val goal = prop_of (#goal (Proof.goal state))
     1.5          val facts = nearly_all_facts ctxt false fact_override Symtab.empty
     1.6                                       Termtab.empty [] [] goal
     1.7 -        val do_learn = mash_learn_proof ctxt params (hd provers) goal facts
     1.8 -      in run_minimize params do_learn i (#add fact_override) state end
     1.9 +        fun learn prover = mash_learn_proof ctxt params prover goal facts
    1.10 +      in run_minimize params learn i (#add fact_override) state end
    1.11      else if subcommand = messagesN then
    1.12        messages opt_i
    1.13      else if subcommand = supported_proversN then