# HG changeset patch
# User wenzelm
# Date 1357597236 -3600
# Node ID ba79e2cb3cbee6d01fa104c8fccbbff62542171c
# Parent  2bbc7ae806344b222d425fae106724b4a4336717# Parent  495ae21b0958bc4aef8a5fba9e7ca1c1fe09c479
merged;

diff -r 2bbc7ae80634 -r ba79e2cb3cbe src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jan 07 22:21:56 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jan 07 23:20:36 2013 +0100
@@ -2127,10 +2127,10 @@
 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
    of monomorphization). The TPTP explicitly forbids name clashes, and some of
    the remote provers might care. *)
-fun line_for_fact ctxt prefix encode freshen pos mono type_enc rank
+fun line_for_fact ctxt prefix encode alt freshen pos mono type_enc rank
         (j, {name, stature = (_, status), role, iformula, atomic_types}) =
   Formula ((prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
-            encode name, name),
+            encode name, alt name),
            role,
            iformula
            |> formula_from_iformula ctxt mono type_enc
@@ -2728,14 +2728,14 @@
       |> lines_for_sym_decl_table ctxt mono type_enc mono_Ts
     val num_facts = length facts
     val fact_lines =
-      map (line_for_fact ctxt fact_prefix ascii_of (not exporter)
+      map (line_for_fact ctxt fact_prefix ascii_of I (not exporter)
                (not exporter) mono type_enc (rank_of_fact_num num_facts))
           (0 upto num_facts - 1 ~~ facts)
     val subclass_lines = maps (lines_for_subclass_pair type_enc) subclass_pairs
     val tcon_lines = map (line_for_tcon_clause type_enc) tcon_clauses
     val helper_lines =
       0 upto length helpers - 1 ~~ helpers
-      |> map (line_for_fact ctxt helper_prefix I false true mono type_enc
+      |> map (line_for_fact ctxt helper_prefix I (K "") false true mono type_enc
                             (K default_rank))
     val free_type_lines = lines_for_free_types type_enc (facts @ conjs)
     val conj_lines = map (line_for_conjecture ctxt mono type_enc) conjs
diff -r 2bbc7ae80634 -r ba79e2cb3cbe src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jan 07 22:21:56 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jan 07 23:20:36 2013 +0100
@@ -968,23 +968,25 @@
 val smt_slice_min_secs =
   Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 5)
 
-fun smt_filter_loop ctxt name
+fun smt_filter_loop name
                     ({debug, verbose, overlord, max_mono_iters,
                       max_new_mono_instances, timeout, slice, ...} : params)
                     state goal i =
   let
+    fun repair_context ctxt =
+      ctxt |> select_smt_solver name
+           |> Config.put SMT_Config.verbose debug
+           |> (if overlord then
+                 Config.put SMT_Config.debug_files
+                            (overlord_file_location_for_prover name
+                             |> (fn (path, name) => path ^ "/" ^ name))
+               else
+                 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)
     val max_slices = if slice then Config.get ctxt smt_max_slices else 1
-    val repair_context =
-      select_smt_solver name
-      #> Config.put SMT_Config.verbose debug
-      #> (if overlord then
-            Config.put SMT_Config.debug_files
-                       (overlord_file_location_for_prover name
-                        |> (fn (path, name) => path ^ "/" ^ name))
-          else
-            I)
-      #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
-    val state = state |> Proof.map_context repair_context
     fun do_slice timeout slice outcome0 time_so_far facts =
       let
         val timer = Timer.startRealTimer ()
@@ -1080,7 +1082,7 @@
     val facts = facts ~~ (0 upto num_facts - 1)
                 |> map (smt_weighted_fact ctxt num_facts)
     val {outcome, used_facts = used_pairs, run_time} =
-      smt_filter_loop ctxt name params state goal subgoal facts
+      smt_filter_loop name params state goal subgoal facts
     val used_facts = used_pairs |> map fst
     val outcome = outcome |> Option.map failure_from_smt_failure
     val (preplay, message, message_tail) =