fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri May 27 10:30:07 2011 +0200
@@ -390,7 +390,7 @@
     val relevance_fudge =
       Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
     val relevance_override = {add = [], del = [], only = false}
-    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
+    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal ctxt goal i
     val time_limit =
       (case hard_timeout of
         NONE => I

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri May 27 10:30:07 2011 +0200
@@ -128,7 +128,8 @@
                (Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover)
          val relevance_override = {add = [], del = [], only = false}
          val subgoal = 1
-         val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
+         val (_, hyp_ts, concl_t) =
+           Sledgehammer_Util.strip_subgoal ctxt goal subgoal
          val facts =
            Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
                (the_default default_max_relevant max_relevant)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri May 27 10:30:07 2011 +0200
@@ -1018,7 +1018,7 @@
         (metis_params as (_, _, type_sys, atp_proof, facts_offset, fact_names,
                           typed_helpers, goal, i)) =
   let
-    val (params, hyp_ts, concl_t) = strip_subgoal goal i
+    val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal i
     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
     val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
     val full_types = uses_typed_helpers typed_helpers atp_proof

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri May 27 10:30:07 2011 +0200
@@ -47,6 +47,7 @@
                  isar_shrink_factor, ...} : params)
         explicit_apply_opt silent (prover : prover) timeout i n state facts =
   let
+    val ctxt = Proof.context_of state
     val thy = Proof.theory_of state
     val _ =
       print silent (fn () =>
@@ -58,7 +59,7 @@
       case explicit_apply_opt of
         SOME explicit_apply => explicit_apply
       | NONE =>
-        let val (_, hyp_ts, concl_t) = strip_subgoal goal i in
+        let val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i in
           not (forall (Meson.is_fol_term thy)
                       (concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
         end

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:07 2011 +0200
@@ -479,7 +479,7 @@
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
-    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
+    val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
     val (dest_dir, problem_prefix) =
       if overlord then overlord_file_location_for_prover name
       else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:07 2011 +0200
@@ -184,7 +184,7 @@
         state |> Proof.map_context (Config.put SMT_Config.verbose debug)
       val ctxt = Proof.context_of state
       val {facts = chained_ths, goal, ...} = Proof.goal state
-      val (_, hyp_ts, concl_t) = strip_subgoal goal i
+      val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
       val _ = () |> not blocking ? kill_provers
       val _ = case find_first (not o is_prover_supported ctxt) provers of
                 SOME name => error ("No such prover: " ^ name ^ ".")

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri May 27 10:30:07 2011 +0200
@@ -28,7 +28,8 @@
   val transform_elim_prop : term -> term
   val specialize_type : theory -> (string * typ) -> term -> term
   val subgoal_count : Proof.state -> int
-  val strip_subgoal : thm -> int -> (string * typ) list * term list * term
+  val strip_subgoal :
+    Proof.context -> thm -> int -> (string * typ) list * term list * term
   val reserved_isar_keyword_table : unit -> unit Symtab.table
 end;
 
@@ -237,12 +238,14 @@
 
 val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
 
-fun strip_subgoal goal i =
+fun strip_subgoal ctxt goal i =
   let
-    val (t, frees) = Logic.goal_params (prop_of goal) i
+    val (t, (frees, params)) =
+      Logic.goal_params (prop_of goal) i
+      ||> (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 (map dest_Free frees), hyp_ts, concl_t) end
+  in (rev params, hyp_ts, concl_t) end
 
 fun reserved_isar_keyword_table () =
   union (op =) (Keyword.dest_keywords ()) (Keyword.dest_commands ())

--- a/src/HOL/ex/sledgehammer_tactics.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML	Fri May 27 10:30:07 2011 +0200
@@ -31,7 +31,7 @@
     val relevance_fudge =
       Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
     val relevance_override = {add = [], del = [], only = false}
-    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
+    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal ctxt goal i
     val facts =
       Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
           (the_default default_max_relevant max_relevant) (K true)