# HG changeset patch # User blanchet # Date 1378732924 -7200 # Node ID 8c3ccb31446950f8e97f71db43f4e01d96d6489c # Parent 75a0427df7a808ad92fb7f02eebdff43db18caa1 use new monomorphizer in Sledgehammer diff -r 75a0427df7a8 -r 8c3ccb314469 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Sep 09 14:23:04 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Sep 09 15:22:04 2013 +0200 @@ -650,14 +650,6 @@ | _ => (maybe_isar_name, []) in minimize_command override_params min_name end -fun repair_legacy_monomorph_context max_iters best_max_iters max_new_instances - best_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 Legacy_Monomorph.keep_partial_instances false - 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) @@ -757,7 +749,7 @@ let val ctxt = ctxt - |> repair_legacy_monomorph_context max_mono_iters + |> repair_monomorph_context max_mono_iters best_max_mono_iters max_new_mono_instances best_max_new_mono_instances (* pseudo-theorem involving the same constants as the subgoal *) @@ -770,9 +762,8 @@ |> op @ |> cons (0, subgoal_th) in - Legacy_Monomorph.monomorph atp_schematic_consts_of rths ctxt - |> fst |> tl - |> curry ListPair.zip (map fst facts) + Monomorph.monomorph atp_schematic_consts_of ctxt rths + |> tl |> curry ListPair.zip (map fst facts) |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) end