src/HOL/Tools/Nitpick/nitpick_nut.ML
changeset 59058 a78612c67ec0
parent 59038 e50f1973cb0a
child 60352 d46de31a50c4
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -765,7 +765,7 @@
       else if is_Cst True u2 then u1
       else raise SAME ()
     | Eq =>
-      (case pairself (is_Cst Unrep) (u1, u2) of
+      (case apply2 (is_Cst Unrep) (u1, u2) of
          (true, true) => unknown_boolean T R
        | (false, false) => raise SAME ()
        | _ => if forall (is_opt_rep o rep_of) [u1, u2] then raise SAME ()