1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4      fun really_go () =
     1.5        problem
     1.6        |> get_minimizing_prover ctxt mode
     1.7 -             (mash_learn_proof ctxt params (prop_of goal)
     1.8 +             (mash_learn_proof ctxt params name (prop_of goal)
     1.9                                 (map untranslated_fact facts))
    1.10               name params minimize_command
    1.11        |> (fn {outcome, preplay, message, message_tail, ...} =>