# 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