# HG changeset patch
# User blanchet
# Date 1357128887 -3600
# Node ID eaa540986291951d863a7bef8a680c1d57a4fa85
# Parent  84c7cf36b2e07799b0e820bc15e5bd6e5f6ef20f
properly take the existential closure of skolems

diff -r 84c7cf36b2e0 -r eaa540986291 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jan 02 10:54:36 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jan 02 13:14:47 2013 +0100
@@ -77,8 +77,13 @@
                   |> lam_trans <> metis_default_lam_trans ? cons lam_trans
   in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
 
-fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
-fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
+fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s
+  | term_name' t = ""
+
+fun lambda' v = Term.lambda_name (term_name' v, v)
+
+fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda' v t
+fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda' v t
 
 fun make_tfree ctxt w =
   let val ww = "'" ^ w in
@@ -248,7 +253,9 @@
                 case unprefix_and_unascii schematic_var_prefix s of
                   SOME s => Var ((s, var_index), T)
                 | NONE =>
-                  Var ((s |> textual ? repair_variable_name Char.toLower,
+                  Var ((s |> textual
+                          ? (repair_variable_name Char.toLower
+                             #> Char.isLower (String.sub (s, 0)) ? Name.skolem),
                         var_index), T)
           in list_comb (t, ts) end
   in do_term [] end
diff -r 84c7cf36b2e0 -r eaa540986291 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Jan 02 10:54:36 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Jan 02 13:14:47 2013 +0100
@@ -644,6 +644,7 @@
         val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph
         val axioms = axioms_of_ref_graph ref_graph conjs
         val tainted = tainted_atoms_of_ref_graph ref_graph conjs
+        val is_skolem = can (try (apfst (apfst Name.dest_skolem)))
         val props =
           Symtab.empty
           |> fold (fn Definition_Step _ => I (* FIXME *)
@@ -653,9 +654,11 @@
                           t |> role <> Conjecture ? s_not
                             |> fold exists_of (map Var (Term.add_vars t []))
                         else
-                          t))
+                          t |> fold exists_of (map Var (filter is_skolem
+                                 (Term.add_vars t [])))))
                   atp_proof
-        (* The assumptions and conjecture are props; the rest are bools. *)
+        (* The assumptions and conjecture are "prop"s; the other formulas are
+           "bool"s. *)
         fun prop_of_clause [name as (s, ss)] =
             (case resolve_conjecture ss of
                [j] => if j = length hyp_ts then concl_t else nth hyp_ts j
@@ -715,18 +718,19 @@
           else
             ""
         | _ =>
-          let 
-            val msg = 
-              (if preplay then 
-                [if preplay_fail 
-                 then "may fail" 
+          let
+            val msg =
+              (if preplay then
+                [if preplay_fail then "may fail"
                  else string_from_ext_time ext_time]
-               else [])
-              @ 
-               (if verbose then
-                  [let val num_steps = metis_steps_total isar_proof
-                   in string_of_int num_steps ^ plural_s num_steps end]
-                else [])
+               else
+                 []) @
+              (if verbose then
+                 let val num_steps = metis_steps_total isar_proof in
+                   [string_of_int num_steps ^ " step" ^ plural_s num_steps]
+                 end
+               else
+                 [])
           in
             "\n\nStructured proof "
               ^ (commas msg |> not (null msg) ? enclose "(" ")")