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 =