src/HOL/Tools/Metis/metis_tactics.ML

            (verbose_warning ctxt
                 ("Falling back on " ^
                  quote (method_call_for_type_enc fallback_type_syss) ^ "...");
             FOL_SOLVE fallback_type_syss ctxt cls ths0)
 
-val neg_clausify =
+fun neg_clausify ctxt =
   single
-  #> Meson.make_clauses_unsorted
+  #> Meson.make_clauses_unsorted ctxt
   #> map Meson_Clausify.introduce_combinators_in_theorem
   #> Meson.finish_cnf
 
 fun preskolem_tac ctxt st0 =
   (if exists (Meson.has_too_many_clauses ctxt)

   in
     if exists_type type_has_top_sort (prop_of st0) then
       verbose_warning ctxt "Proof state contains the universal sort {}"
     else
       ();
-    Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
+    Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt)) tac ctxt i st0
   end
 
 fun metis_tac [] = generic_metis_tac partial_type_syss
   | metis_tac type_syss = generic_metis_tac type_syss