src/HOL/Tools/ATP_Manager/atp_systems.ML
changeset 36910 dd5a31098f85
parent 36568 d495d2e1f0a6
child 36917 8674cdb0b8cc
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri May 14 11:23:42 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri May 14 11:24:14 2010 +0200
@@ -215,8 +215,8 @@
       case outcome of
         NONE =>
         proof_text isar_proof
-                   (pool, debug, shrink_factor, ctxt, conjecture_shape)
-                   (minimize_command, proof, internal_thm_names, th, subgoal)
+            (pool, debug, full_types, shrink_factor, ctxt, conjecture_shape)
+            (minimize_command, proof, internal_thm_names, th, subgoal)
       | SOME failure => (string_for_failure failure ^ "\n", [])
   in
     {outcome = outcome, message = message, pool = pool,