# HG changeset patch
# User blanchet
# Date 1368709110 -7200
# Node ID 11b48e7a4e7e079306efbf133f39dc8f1d572bbd
# Parent  047bb4a9466c434f87f067b522333e178f376d61
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer

diff -r 047bb4a9466c -r 11b48e7a4e7e src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu May 16 14:27:43 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu May 16 14:58:30 2013 +0200
@@ -78,7 +78,7 @@
   in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
 
 fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s
-  | term_name' t = ""
+  | term_name' _ = ""
 
 fun lambda' v = Term.lambda_name (term_name' v, v)
 
diff -r 047bb4a9466c -r 11b48e7a4e7e src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 16 14:27:43 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 16 14:58:30 2013 +0200
@@ -640,13 +640,20 @@
       | _ => (maybe_isar_name, [])
   in minimize_command override_params min_name end
 
-fun repair_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)
+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)
+  #> Config.put Monomorph.max_new_instances
+         (max_new_instances |> the_default best_max_new_instances)
+
 fun suffix_of_mode Auto_Try = "_try"
   | suffix_of_mode Try = "_try"
   | suffix_of_mode Normal = ""
@@ -737,8 +744,9 @@
           let
             val ctxt =
               ctxt
-              |> repair_monomorph_context max_mono_iters best_max_mono_iters
-                      max_new_mono_instances best_max_new_mono_instances
+              |> repair_legacy_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 *)
             val subgoal_th =
               Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
@@ -837,7 +845,7 @@
               |> lines_of_atp_problem format ord ord_info
               |> cons ("% " ^ command ^ "\n")
               |> File.write_list prob_path
-            val ((output, run_time), used_from, (atp_proof, outcome)) =
+            val ((output, run_time), (atp_proof, outcome)) =
               time_limit generous_slice_timeout Isabelle_System.bash_output
                          command
               |>> (if overlord then
@@ -846,14 +854,14 @@
                      I)
               |> fst |> split_time
               |> (fn accum as (output, _) =>
-                     (accum, facts,
+                     (accum,
                       extract_tstplike_proof_and_outcome verbose proof_delims
                                                          known_failures output
                       |>> atp_proof_of_tstplike_proof atp_problem
                       handle UNRECOGNIZED_ATP_PROOF () =>
                              ([], SOME ProofIncomplete)))
               handle TimeLimit.TimeOut =>
-                     (("", the slice_timeout), [], ([], SOME TimedOut))
+                     (("", the slice_timeout), ([], SOME TimedOut))
             val outcome =
               case outcome of
                 NONE =>
@@ -1029,18 +1037,15 @@
                  I)
            |> Config.put SMT_Config.infer_triggers
                          (Config.get ctxt smt_triggers)
-    val ctxt = Proof.context_of state |> repair_context
-    val state = state |> Proof.map_context (K ctxt)
+           |> repair_monomorph_context max_mono_iters default_max_mono_iters
+                  max_new_mono_instances default_max_new_mono_instances
+    val state = Proof.map_context (repair_context) state
+    val ctxt = Proof.context_of state
     val max_slices = if slice then Config.get ctxt smt_max_slices else 1
     fun do_slice timeout slice outcome0 time_so_far
                  (weighted_factss as (fact_filter, weighted_facts) :: _) =
       let
         val timer = Timer.startRealTimer ()
-        val state =
-          state |> Proof.map_context
-                       (repair_monomorph_context max_mono_iters
-                            default_max_mono_iters max_new_mono_instances
-                            default_max_new_mono_instances)
         val slice_timeout =
           if slice < max_slices andalso timeout <> NONE then
             let val ms = timeout |> the |> Time.toMilliseconds in
diff -r 047bb4a9466c -r 11b48e7a4e7e src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu May 16 14:27:43 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu May 16 14:58:30 2013 +0200
@@ -284,7 +284,7 @@
       apsnd (union (op =) (map fst (resolve_fact fact_names ss)))
     else
       apfst (insert (op =) (label_of_clause names))
-  | add_fact_of_dependencies fact_names names =
+  | add_fact_of_dependencies _ names =
     apfst (insert (op =) (label_of_clause names))
 
 fun repair_name "$true" = "c_True"