1.1 --- a/src/HOL/Tools/atp_minimal.ML	Tue Jul 21 00:56:19 2009 +0200
     1.2 +++ b/src/HOL/Tools/atp_minimal.ML	Tue Jul 21 01:03:18 2009 +0200
     1.3 @@ -125,7 +125,8 @@
     1.4        println ("Minimize called with " ^ length_string name_thms_pairs ^ " theorems, prover: "
     1.5          ^ prover_name ^ ", time limit: " ^ Int.toString time_limit ^ " seconds")
     1.6      val _ = debug_fn (fn () => app (fn (n, tl) =>
     1.7 -        (debug n; app (fn t => debug ("  " ^ Display.string_of_thm t)) tl)) name_thms_pairs)
     1.8 +        (debug n; app (fn t =>
     1.9 +          debug ("  " ^ Display.string_of_thm (Proof.context_of state) t)) tl)) name_thms_pairs)
    1.10      val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
    1.11      fun test_thms filtered thms =
    1.12        case test_thms_fun filtered thms of (Success _, _) => true | _ => false