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/sledgehammer_filter.ML
changeset 43581 c3e4d280bdeb
parent 43576 ebeda6275027
parent 43559 c1966f322105
child 44400 01b8b6fcd857 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Jun 27 17:04:04 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Jun 27 22:44:44 2011 +0200
@@ -320,7 +320,7 @@
       do_formula pos body_t
       #> (if also_skolems andalso will_surely_be_skolemized then
             add_pconst_to_table true
-                (gensym skolem_prefix, PType (order_of_type abs_T, []))
+                (legacy_gensym skolem_prefix, PType (order_of_type abs_T, []))
           else
             I)
     and do_term_or_formula ext_arg T =
isabelle