changeset 36289 | f75b6a3e1450 |
parent 36287 | 96f45c5ffb36 |
child 36369 | d2cd0d04b8e6 |
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Apr 22 15:01:36 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Apr 22 16:30:04 2010 +0200 @@ -122,7 +122,7 @@ ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".") in (SOME min_thms, - proof_text true isar_proof debug modulus sorts ctxt + proof_text isar_proof debug modulus sorts ctxt (K "", proof, internal_thm_names, goal, i) |> fst) end | (Timeout, _) =>