src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
changeset 43559 c1966f322105
parent 43492 43326cadc31a
child 43581 c3e4d280bdeb
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Jun 27 15:01:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Jun 27 15:03:55 2011 +0200
     1.3 @@ -320,7 +320,7 @@
     1.4        do_formula pos body_t
     1.5        #> (if also_skolems andalso will_surely_be_skolemized then
     1.6              add_pconst_to_table true
     1.7 -                (gensym skolem_prefix, PType (order_of_type abs_T, []))
     1.8 +                (legacy_gensym skolem_prefix, PType (order_of_type abs_T, []))
     1.9            else
    1.10              I)
    1.11      and do_term_or_formula ext_arg T =