src/HOL/Tools/Metis/metis_generate.ML

       map2 (fn j => pair (Int.toString j, (Local, Simp))) (0 upto num_conjs - 1) conj_clauses @
       map2 (fn j => pair (Int.toString (num_conjs + j), (Local, Simp)))
         (0 upto length fact_clauses - 1) fact_clauses
     val (old_skolems, props) =
       fold_rev (fn (name, th) => fn (old_skolems, props) =>
-           th |> prop_of |> Logic.strip_imp_concl
+           th |> Thm.prop_of |> Logic.strip_imp_concl
               |> conceal_old_skolem_terms (length clauses) old_skolems
               ||> (lam_trans = liftingN orelse lam_trans = lam_liftingN) ? eliminate_lam_wrappers
               ||> (fn prop => (name, prop) :: props))
          clauses ([], [])
     (*