--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu May 12 15:29:18 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu May 12 15:29:18 2011 +0200
@@ -42,8 +42,9 @@
fun print silent f = if silent then () else Output.urgent_message (f ())
-fun test_facts ({debug, verbose, overlord, provers, monomorphize_limit,
- type_sys, isar_proof, isar_shrink_factor, ...} : params)
+fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
+ max_mono_instances, type_sys, isar_proof, isar_shrink_factor,
+ ...} : params)
explicit_apply_opt silent (prover : prover) timeout i n state facts =
let
val thy = Proof.theory_of state
@@ -65,9 +66,9 @@
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
- monomorphize_limit = monomorphize_limit, isar_proof = isar_proof,
- isar_shrink_factor = isar_shrink_factor, slicing = false,
- timeout = timeout, expect = ""}
+ max_mono_iters = max_mono_iters, max_mono_instances = max_mono_instances,
+ isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
+ slicing = false, timeout = timeout, expect = ""}
val facts =
facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
val problem =