--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Mar 28 22:42:18 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Mar 28 23:44:41 2013 +0100
@@ -640,10 +640,10 @@
fun repair_monomorph_context max_iters best_max_iters max_new_instances
best_max_new_instances =
- Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
- #> Config.put Monomorph.max_new_instances
+ Config.put Legacy_Monomorph.max_rounds (max_iters |> the_default best_max_iters)
+ #> Config.put Legacy_Monomorph.max_new_instances
(max_new_instances |> the_default best_max_new_instances)
- #> Config.put Monomorph.keep_partial_instances false
+ #> Config.put Legacy_Monomorph.keep_partial_instances false
fun suffix_for_mode Auto_Try = "_try"
| suffix_for_mode Try = "_try"
@@ -747,7 +747,7 @@
|> op @
|> cons (0, subgoal_th)
in
- Monomorph.monomorph atp_schematic_consts_of rths ctxt |> fst |> tl
+ Legacy_Monomorph.monomorph atp_schematic_consts_of rths ctxt |> fst |> tl
|> curry ListPair.zip (map fst facts)
|> maps (fn (name, rths) =>
map (pair name o zero_var_indexes o snd) rths)