--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri May 14 22:28:39 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri May 14 22:29:50 2010 +0200
@@ -112,8 +112,8 @@
fun generic_prover overlord get_facts prepare write_file home_var executable
args proof_delims known_failures name
- ({debug, full_types, explicit_apply, isar_proof, shrink_factor, ...}
- : params) minimize_command
+ ({debug, full_types, explicit_apply, isar_proof, isar_shrink_factor,
+ ...} : params) minimize_command
({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
: problem) =
let
@@ -218,7 +218,8 @@
case outcome of
NONE =>
proof_text isar_proof
- (pool, debug, full_types, shrink_factor, ctxt, conjecture_shape)
+ (pool, debug, full_types, isar_shrink_factor, ctxt,
+ conjecture_shape)
(minimize_command, proof, internal_thm_names, th, subgoal)
| SOME failure => (string_for_failure failure ^ "\n", [])
in