--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Apr 22 13:50:58 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Apr 22 14:47:52 2010 +0200
@@ -122,8 +122,8 @@
["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
in
(SOME min_thms,
- proof_text isar_proof debug modulus sorts ctxt (K "") proof
- internal_thm_names goal i |> fst)
+ proof_text true isar_proof debug modulus sorts ctxt
+ (K "", proof, internal_thm_names, goal, i) |> fst)
end
| (Timeout, _) =>
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \