src/HOL/Library/Old_SMT/old_smt_normalize.ML

 
   fun minimal_pats vs ct =
     if has_all_vars vs (Thm.term_of ct) then
       (case Thm.term_of ct of
         _ $ _ =>
-          (case pairself (minimal_pats vs) (Thm.dest_comb ct) of
+          (case apply2 (minimal_pats vs) (Thm.dest_comb ct) of
             ([], []) => [[ct]]
           | (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss')
       | _ => [])
     else []
 

 
   val pat =
     Old_SMT_Utils.mk_const_pat @{theory} @{const_name pat} Old_SMT_Utils.destT1
   fun mk_pat ct = Thm.apply (Old_SMT_Utils.instT' ct pat) ct
 
-  fun mk_clist T = pairself (Thm.cterm_of @{theory})
+  fun mk_clist T = apply2 (Thm.cterm_of @{theory})
     (HOLogic.cons_const T, HOLogic.nil_const T)
   fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
   val mk_pat_list = mk_list (mk_clist @{typ pattern})
   val mk_mpat_list = mk_list (mk_clist @{typ "pattern list"})  
   fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss