# HG changeset patch
# User blanchet
# Date 1273829054 -7200
# Node ID dd5a31098f8553da803216eeb7b85cea8523bccd
# Parent  7d5587f6d5f7ab3f84e69bf93e96b8776ee1a69f
pass "full_type" argument to proof reconstruction

diff -r 7d5587f6d5f7 -r dd5a31098f85 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- 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,