src/HOL/Tools/Metis/metis_translate.ML

               #> rpair ctxt
               #-> Monomorph.monomorph Monomorph.all_schematic_consts_of
               #> fst #> maps (map (zero_var_indexes o snd)))
       val (old_skolems, props) =
         fold_rev (fn clause => fn (old_skolems, props) =>
-                     conceal_old_skolem_terms (length clauses) old_skolems
-                                              (prop_of clause)
-                     ||> (fn prop => prop :: props))
+                     clause |> prop_of |> Logic.strip_imp_concl
+                            |> conceal_old_skolem_terms (length clauses)
+                                                        old_skolems
+                            ||> (fn prop => prop :: props))
              clauses ([], [])
       val (atp_problem, _, _, _, _, _, sym_tab) =
         prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
                             false false props @{prop False} []
       val axioms =