--- a/src/Tools/nbe.ML Thu Nov 04 17:27:37 2010 +0100
+++ b/src/Tools/nbe.ML Thu Nov 04 17:27:38 2010 +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 (Code.check_const thy)) lhs_rhs
+ val c_c' = case try (pairself (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);