src/HOL/Tools/Lifting/lifting_def.ML

             else
               subst
           end;
         
         val subst = fold make_subst free_vars [];
-        val csubst = map (pairself (cterm_of thy)) subst;
+        val csubst = map (apply2 (cterm_of thy)) subst;
         val inst_thm = Drule.cterm_instantiate csubst thm;
       in
         Conv.fconv_rule 
           ((Conv.concl_conv (nprems_of inst_thm) o HOLogic.Trueprop_conv o Conv.fun2_conv o Conv.arg1_conv)
             (Raw_Simplifier.rewrite ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm