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 47022 8eac39af4ec0
parent 46976 80123a220219
child 47073 c73f7b0c7ebc 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Mar 19 20:32:57 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Mar 19 21:10:33 2012 +0100
@@ -374,7 +374,7 @@
       do_formula pos body_t
       #> (if also_skolems andalso will_surely_be_skolemized then
             add_pconst_to_table true
-                (legacy_gensym skolem_prefix, PType (order_of_type abs_T, []))
+                (Misc_Legacy.gensym skolem_prefix, PType (order_of_type abs_T, []))
           else
             I)
     and do_term_or_formula ext_arg T =
isabelle