src/HOL/Tools/ATP_Manager/atp_minimal.ML
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, _) =>