--- 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,