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 ()