# HG changeset patch
# User blanchet
# Date 1403590762 -7200
# Node ID ffd928316c75451ae17dfc8b8d4af702e3dba10b
# Parent  68aa585269acbad9d7d3eb4872e25adbd3953d6e
supports gradual skolemization (cf. Z3) by threading context through correctly

diff -r 68aa585269ac -r ffd928316c75 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jun 24 08:19:22 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jun 24 08:19:22 2014 +0200
@@ -141,8 +141,8 @@
         val do_preplay = preplay_timeout <> Time.zeroTime
         val compress = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress
 
-        val is_fixed = Variable.is_declared ctxt orf Name.is_skolem
-        fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
+        fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem
+        fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev
 
         fun get_role keep_role ((num, _), role, t, rule, _) =
           if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
@@ -157,18 +157,21 @@
               if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE)
             atp_proof
         val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof
-        val lems =
-          map_filter (get_role (curry (op =) Lemma)) atp_proof
-          |> map (fn ((l, t), rule) =>
-            let
-              val (skos, meths) =
-                (if is_skolemize_rule rule then (skolems_of t, skolem_methods)
-                 else if is_arith_rule rule then ([], arith_methods)
-                 else ([], rewrite_methods))
-                ||> massage_methods
-            in
-              Prove ([], skos, l, t, [], ([], []), meths, "")
-            end)
+
+        fun add_lemma ((l, t), rule) ctxt =
+          let
+            val (skos, meths) =
+              (if is_skolemize_rule rule then (skolems_of ctxt t, skolem_methods)
+               else if is_arith_rule rule then ([], arith_methods)
+               else ([], rewrite_methods))
+              ||> massage_methods
+          in
+            (Prove ([], skos, l, t, [], ([], []), meths, ""),
+             ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd))
+          end
+
+        val (lems, _) =
+          fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt
 
         val bot = atp_proof |> List.last |> #1
 
@@ -242,15 +245,16 @@
                 (case gamma of
                   [g] =>
                   if skolem andalso is_clause_tainted g then
-                    let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
+                    let val subproof = Proof (skolems_of ctxt (prop_of_clause g), [], rev accum) in
                       isar_steps outer (SOME l) [prove [subproof] ([], [])] infs
                     end
                   else
                     steps_of_rest (prove [] deps)
                 | _ => steps_of_rest (prove [] deps))
               else
-                steps_of_rest (if skolem then Prove ([], skolems_of t, l, t, [], deps, meths, "")
-                  else prove [] deps)
+                steps_of_rest
+                  (if skolem then Prove ([], skolems_of ctxt t, l, t, [], deps, meths, "")
+                   else prove [] deps)
             end
           | isar_steps outer predecessor accum (Cases cases :: infs) =
             let