redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue May 28 08:36:12 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue May 28 08:52:41 2013 +0200
@@ -454,7 +454,7 @@
       Sledgehammer_Provers.default_max_facts_of_prover ctxt slice prover_name
     val is_appropriate_prop =
       Sledgehammer_Provers.is_appropriate_prop_of_prover ctxt prover_name
-    val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal i ctxt
+    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
     val time_limit =
       (case hard_timeout of
         NONE => I

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue May 28 08:36:12 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue May 28 08:52:41 2013 +0200
@@ -124,8 +124,7 @@
            extract_relevance_fudge args
                (Sledgehammer_Provers.relevance_fudge_of_prover ctxt prover)
          val subgoal = 1
-         val ((_, hyp_ts, concl_t), ctxt) =
-           ATP_Util.strip_subgoal goal subgoal ctxt
+         val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt
          val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
          val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
          val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt

--- a/src/HOL/TPTP/mash_eval.ML	Tue May 28 08:36:12 2013 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Tue May 28 08:52:41 2013 +0200
@@ -109,7 +109,7 @@
               SOME (_, th) => th
             | NONE => error ("No fact called \"" ^ name ^ "\".")
           val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
-          val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal 1 ctxt
+          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
           val isar_deps = isar_dependencies_of name_tabs th
           val facts =
             facts

--- a/src/HOL/TPTP/mash_export.ML	Tue May 28 08:36:12 2013 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Tue May 28 08:52:41 2013 +0200
@@ -207,7 +207,7 @@
           val name = nickname_of_thm th
           val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
           val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
-          val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal 1 ctxt
+          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
           val isar_deps = isar_dependencies_of name_tabs th
         in
           if is_bad_query ctxt ho_atp step j th isar_deps then

--- a/src/HOL/TPTP/sledgehammer_tactics.ML	Tue May 28 08:36:12 2013 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Tue May 28 08:52:41 2013 +0200
@@ -32,7 +32,7 @@
     val name = hd provers
     val prover = get_prover ctxt mode name
     val default_max_facts = default_max_facts_of_prover ctxt slice name
-    val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal i ctxt
+    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
     val ho_atp = exists (is_ho_atp ctxt) provers
     val reserved = reserved_isar_keyword_table ()
     val css_table = clasimpset_rule_table_of ctxt

--- a/src/HOL/Tools/ATP/atp_util.ML	Tue May 28 08:36:12 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Tue May 28 08:52:41 2013 +0200
@@ -49,8 +49,7 @@
   val transform_elim_prop : term -> term
   val specialize_type : theory -> (string * typ) -> term -> term
   val strip_subgoal :
-    thm -> int -> Proof.context
-    -> ((string * typ) list * term list * term) * Proof.context
+    thm -> int -> Proof.context -> (string * typ) list * term list * term
 end;
 
 structure ATP_Util : ATP_UTIL =
@@ -432,17 +431,11 @@
 
 fun strip_subgoal goal i ctxt =
   let
-    val (t, ((frees, params), ctxt)) =
+    val (t, (frees, params)) =
       Logic.goal_params (prop_of goal) i
-      ||> map dest_Free
-      ||> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
-      ||> (fn fixes =>
-              ctxt |> Variable.set_body false
-                   |> Proof_Context.add_fixes fixes
-                   |>> map2 (fn (_, SOME T, _) => fn s => (s, T)) fixes)
-      ||> apfst (`(map Free))
+      ||> (map dest_Free #> Variable.variant_frees ctxt [] #> `(map Free))
     val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
     val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
-  in ((rev params, hyp_ts, concl_t), ctxt) end
+  in (rev params, hyp_ts, concl_t) end
 
 end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue May 28 08:36:12 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue May 28 08:52:41 2013 +0200
@@ -707,7 +707,7 @@
     let
       val thy = Proof_Context.theory_of ctxt
       val goal = goal_of_thm thy th
-      val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal 1 ctxt
+      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
       val facts = facts |> filter (fn (_, th') => thm_less (th', th))
       fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th)
       fun is_dep dep (_, th) = nickname_of_thm th = dep

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 28 08:36:12 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 28 08:52:41 2013 +0200
@@ -686,7 +686,7 @@
     val atp_mode =
       if Config.get ctxt completish then Sledgehammer_Completish
       else Sledgehammer
-    val ((_, hyp_ts, concl_t), ctxt') = strip_subgoal goal subgoal ctxt
+    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
     val (dest_dir, problem_prefix) =
       if overlord then overlord_file_location_of_prover name
       else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue May 28 08:36:12 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue May 28 08:52:41 2013 +0200
@@ -649,7 +649,13 @@
      fact_names, lifted, sym_tab, atp_proof, goal)
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
-    val ((params, hyp_ts, concl_t), ctxt) = strip_subgoal goal subgoal ctxt
+    val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
+    val (_, ctxt) =
+      params
+      |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
+      |> (fn fixes =>
+             ctxt |> Variable.set_body false
+                  |> Proof_Context.add_fixes fixes)
     val one_line_proof = one_line_proof_text 0 one_line_params
     val type_enc =
       if is_typed_helper_used_in_atp_proof atp_proof then full_typesN

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue May 28 08:36:12 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue May 28 08:52:41 2013 +0200
@@ -198,7 +198,7 @@
         state |> Proof.map_context (Config.put SMT_Config.verbose debug)
       val ctxt = Proof.context_of state
       val {facts = chained, goal, ...} = Proof.goal state
-      val ((_, hyp_ts, concl_t), _) = strip_subgoal goal i ctxt
+      val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
       val ho_atp = exists (is_ho_atp ctxt) provers
       val reserved = reserved_isar_keyword_table ()
       val css = clasimpset_rule_table_of ctxt