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 39896 13b3a2ba9ea7
parent 39895 a91a84b1dfdd
child 39939 6e9aff5ee9b5 
--- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Thu Sep 30 19:15:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Thu Sep 30 20:44:53 2010 +0200
@@ -121,7 +121,7 @@
                     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_prefix c then
+                    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)
isabelle