# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 0a72c0527111972b9372e120a9c7610a3f7bc053
# Parent  494fde2077065f3dd85970741bf65a4802570a6f
fixed reconstruction of new Skolem constants in new Metis

diff -r 494fde207706 -r 0a72c0527111 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -470,6 +470,7 @@
               @{const True} (* ignore type predicates *)
             else
               let
+                val new_skolem = String.isPrefix new_skolem_const_prefix s
                 val num_ty_args =
                   length us - the_default 0 (Symtab.lookup sym_tab s)
                 val (type_us, term_us) =
@@ -478,8 +479,12 @@
                 val T =
                   (if not (null type_us) andalso
                       num_type_args thy s' = length type_us then
-                     try (Sign.const_instance thy)
-                         (s', map (typ_from_atp ctxt) type_us)
+                     let val Ts = type_us |> map (typ_from_atp ctxt) in
+                       if new_skolem then
+                         SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts))
+                       else
+                         try (Sign.const_instance thy) (s', Ts)
+                     end
                    else
                      NONE)
                   |> (fn SOME T => T
@@ -487,8 +492,12 @@
                                  (case opt_T of
                                     SOME T => T
                                   | NONE => HOLogic.typeT))
-                val s' = s' |> unproxify_const
-              in list_comb (Const (s', T), term_ts @ extra_ts) end
+                val t =
+                  if new_skolem then
+                    Var ((new_skolem_var_name_from_const s, var_index), T)
+                  else
+                    Const (unproxify_const s', T)
+              in list_comb (t, term_ts @ extra_ts) end
           end
         | NONE => (* a free or schematic variable *)
           let