src/Tools/nbe.ML

     val _ = if Term.add_tvars eqn [] = [tvar] then ()
       else error ("Inconsistent type: " ^ Display.string_of_thm_global thy thm);
     val lhs_rhs = case try Logic.dest_equals eqn
      of SOME lhs_rhs => lhs_rhs
       | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
-    val c_c' = case try (pairself (Axclass.unoverload_const thy o dest_Const)) lhs_rhs
+    val c_c' = case try (apply2 (Axclass.unoverload_const thy o dest_Const)) lhs_rhs
      of SOME c_c' => c_c'
       | _ => error ("Not an equation with two constants: "
           ^ Syntax.string_of_term_global thy eqn);
     val _ = if the_list (Axclass.class_of_param thy (snd c_c')) = [class] then ()
       else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm);