--- a/src/Tools/nbe.ML Wed Nov 26 16:55:43 2014 +0100
+++ b/src/Tools/nbe.ML Wed Nov 26 20:05:34 2014 +0100
@@ -64,7 +64,7 @@
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);