# HG changeset patch
# User blanchet
# Date 1360921686 -3600
# Node ID 2246a2e17f92c2075f6952007bc5bcc2e3a3e528
# Parent  020a6812a204d8f07009d62c9a33d2c0d419697e
tuning -- refactoring in preparation for handling skolemization of conjecture

diff -r 020a6812a204 -r 2246a2e17f92 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Feb 15 10:18:44 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Feb 15 10:48:06 2013 +0100
@@ -697,8 +697,7 @@
                               else
                                 I))))
                   atp_proof
-        fun is_clause_skolemize_rule [atom as (s, _)] =
-            not (member (op =) tainted atom) andalso
+        fun is_clause_skolemize_rule [(s, _)] =
             Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) =
             SOME true
           | is_clause_skolemize_rule _ = false
@@ -724,41 +723,45 @@
         fun maybe_show outer c =
           (outer andalso length c = 1 andalso subset (op =) (c, conjs))
           ? cons Show
-        fun isar_step_of_direct_inf outer (Have (gamma, c)) =
+        fun isar_proof_of_direct_proof _ accum [] = rev accum
+          | isar_proof_of_direct_proof outer accum (inf :: infs) =
             let
-              val l = label_of_clause c
-              val t = prop_of_clause c
-              val by =
-                By_Metis (fold (add_fact_from_dependencies fact_names) gamma
-                               ([], []))
+              fun do_rest step =
+                isar_proof_of_direct_proof outer (step :: accum) infs
+              val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
+              fun skolems_of t =
+                Term.add_frees t [] |> filter_out (is_fixed o fst)
             in
-              if is_clause_skolemize_rule c then
+              case inf of
+                Have (gamma, c) =>
                 let
-                  val is_fixed =
-                    Variable.is_declared ctxt orf can Name.dest_skolem
-                  val xs = Term.add_frees t [] |> filter_out (is_fixed o fst)
-                in Obtain ([], xs, l, t, by) end
-              else
-                Prove (maybe_show outer c [], l, t, by)
+                  val l = label_of_clause c
+                  val t = prop_of_clause c
+                  val by =
+                    By_Metis (fold (add_fact_from_dependencies fact_names) gamma
+                                   ([], []))
+                in
+                  if is_clause_skolemize_rule c andalso
+                     not (member (op =) tainted (the_single c)) then
+                    do_rest (Obtain ([], skolems_of t, l, t, by))
+                  else
+                    do_rest (Prove (maybe_show outer c [], l, t, by))
+                end
+              | Cases cases =>
+                let
+                  fun do_case (c, infs) =
+                    Assume (label_of_clause c, prop_of_clause c) ::
+                    isar_proof_of_direct_proof false [] infs
+                  val c = succedent_of_cases cases
+                  val step =
+                    Prove (maybe_show outer c [Ultimately], label_of_clause c,
+                           prop_of_clause c, Case_Split (map do_case cases))
+                in do_rest step end
             end
-          | isar_step_of_direct_inf outer (Cases cases) =
-            let
-              fun do_case (c, infs) =
-                Assume (label_of_clause c, prop_of_clause c) ::
-                map (isar_step_of_direct_inf false) infs
-              val c = succedent_of_cases cases
-            in
-              Prove (maybe_show outer c [Ultimately], label_of_clause c,
-                     prop_of_clause c, Case_Split (map do_case cases))
-            end
-        fun isar_proof_of_direct_proof direct_proof =
-          direct_proof
-          |> map (isar_step_of_direct_inf true)
-          |> append assms
         val (isar_proof, (preplay_fail, preplay_time)) =
           refute_graph
           |> redirect_graph axioms tainted bot
-          |> isar_proof_of_direct_proof
+          |> isar_proof_of_direct_proof true assms
           |> (if not preplay andalso isar_compress <= 1.0 then
                 rpair (false, (true, seconds 0.0))
               else