src/HOL/Tools/ATP/atp_problem_generate.ML

                     (0 upto length Ts - 1 ~~ Ts))
 
 fun do_introduce_combinators ctxt Ts t =
   let val thy = Proof_Context.theory_of ctxt in
     t |> conceal_bounds Ts
-      |> cterm_of thy
+      |> Thm.cterm_of thy
       |> Meson_Clausify.introduce_combinators_in_cterm
-      |> prop_of |> Logic.dest_equals |> snd
+      |> Thm.prop_of |> Logic.dest_equals |> snd
       |> reveal_bounds Ts
   end
   (* A type variable of sort "{}" will make abstraction fail. *)
   handle THM _ => t |> do_cheaply_conceal_lambdas Ts
 val introduce_combinators = simple_translate_lambdas do_introduce_combinators

 
 fun presimplify_term ctxt t =
   if exists_Const (member (op =) Meson.presimplified_consts o fst) t then
     t |> Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
       |> Meson.presimplify ctxt
-      |> prop_of
+      |> Thm.prop_of
   else
     t
 
 fun preprocess_abstractions_in_terms trans_lams facts =
   let

                   (helper_s <> unmangled_s andalso
                    (not completish orelse could_specialize)) then
                  I
                else
                  ths ~~ (1 upto length ths)
-                 |> maps (dub_and_inst needs_sound o apfst (apsnd prop_of))
+                 |> maps (dub_and_inst needs_sound o apfst (apsnd Thm.prop_of))
                  |> make_facts
                  |> union (op = o apply2 #iformula))
            (if completish then completish_helper_table else helper_table)
     end
   | NONE => I)