# HG changeset patch
# User blanchet
# Date 1286218555 -7200
# Node ID 6e9aff5ee9b5d90e979ee1ebee2715ec57498280
# Parent  0a2091f86eb469bac87ec60d2c1906bd71af214f
paramify new skolems just like old ones (cf. reveal_old_skolem_terms)

diff -r 0a2091f86eb4 -r 6e9aff5ee9b5 src/HOL/Tools/Sledgehammer/metis_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Mon Oct 04 18:31:34 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Mon Oct 04 20:55:55 2010 +0200
@@ -121,10 +121,12 @@
                     val nterms = length ts - ntypes
                     val tts = map tm_to_tt ts
                     val tys = types_of (List.take(tts,ntypes))
-                    val t = if String.isPrefix new_skolem_const_prefix c then
-                              Var (new_skolem_var_from_const c, tl tys ---> hd tys)
-                            else
-                              Const (c, dummyT)
+                    val t =
+                      if String.isPrefix new_skolem_const_prefix c then
+                        Var (new_skolem_var_from_const c,
+                             Type_Infer.paramify_vars (tl tys ---> hd tys))
+                      else
+                        Const (c, dummyT)
                   in if length tys = ntypes then
                          apply_list t nterms (List.drop(tts,ntypes))
                      else