src/HOL/Tools/Metis/metis_translate.ML

               I
             else
               map (pair 0)
               #> rpair ctxt
               #-> Monomorph.monomorph Monomorph.all_schematic_consts_of
-              #> fst #> maps (map snd))
+              #> fst #> maps (map (zero_var_indexes o snd)))
       val (atp_problem, _, _, _, _, _, sym_tab) =
         prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
                             false false (map prop_of clauses) @{prop False} []
       val axioms =
         atp_problem