src/Tools/nbe.ML
changeset 40362 82a066bff182
parent 39911 2b4430847310
child 40564 6827505e96e1
     1.1 --- a/src/Tools/nbe.ML	Thu Nov 04 17:27:37 2010 +0100
     1.2 +++ b/src/Tools/nbe.ML	Thu Nov 04 17:27:38 2010 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4      val lhs_rhs = case try Logic.dest_equals eqn
     1.5       of SOME lhs_rhs => lhs_rhs
     1.6        | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
     1.7 -    val c_c' = case try (pairself (Code.check_const thy)) lhs_rhs
     1.8 +    val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs
     1.9       of SOME c_c' => c_c'
    1.10        | _ => error ("Not an equation with two constants: "
    1.11            ^ Syntax.string_of_term_global thy eqn);