src/HOL/Tools/ATP/atp_problem_generate.ML

                     (0 upto length Ts - 1 ~~ Ts))
 
 fun do_introduce_combinators ctxt Ts t =
   (t |> conceal_bounds Ts
      |> Thm.cterm_of ctxt
-     |> Meson_Clausify.introduce_combinators_in_cterm
+     |> Meson_Clausify.introduce_combinators_in_cterm ctxt
      |> Thm.prop_of |> Logic.dest_equals |> snd
      |> reveal_bounds Ts)
   (* 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