Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/metis_reconstruct.ML
changeset 39939 6e9aff5ee9b5
parent 39896 13b3a2ba9ea7 
--- 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
isabelle