src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML

       | (_, ts) => fold (do_term false) ts
     fun do_quantifier will_surely_be_skolemized abs_T body_t =
       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 =
       if T = HOLogic.boolT then do_formula NONE else do_term ext_arg
     and do_formula pos t =