src/HOL/Tools/Metis/metis_translate.ML

       |> (if polymorphism_of_type_sys type_sys = Polymorphic then
             I
           else
             map (pair 0)
             #> rpair ctxt
-            #-> Monomorph.monomorph Monomorph.all_schematic_consts_of
+            #-> Monomorph.monomorph atp_schematic_consts_of
             #> fst #> maps (map (zero_var_indexes o snd)))
     val (old_skolems, props) =
       fold_rev (fn clause => fn (old_skolems, props) =>
                    clause |> prop_of |> Logic.strip_imp_concl
                           |> conceal_old_skolem_terms (length clauses)