src/Tools/nbe.ML
changeset 59058 a78612c67ec0
parent 58397 1c036d6216d3
child 59151 a012574b78e7
     1.1 --- a/src/Tools/nbe.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/Tools/nbe.ML	Wed Nov 26 20:05:34 2014 +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 (Axclass.unoverload_const thy o dest_Const)) lhs_rhs
     1.8 +    val c_c' = case try (apply2 (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);