# HG changeset patch
# User blanchet
# Date 1284401704 -7200
# Node ID eac5f82eefb6e379bad4832f6130a69018c67cdd
# Parent  1a0e6f16a91b2fc747f15137e49adda70b5c44b4
move equation up where it's not ignored

diff -r 1a0e6f16a91b -r eac5f82eefb6 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Sep 13 20:10:24 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Sep 13 20:15:04 2010 +0200
@@ -653,7 +653,8 @@
     FreeName _ => true
   | Op1 (SingletonSet, _, _, _) => true
   | Op1 (Converse, _, _, u1) => is_fully_representable_set u1
-  | Op2 (oper, _, _, u1, u2) =>
+  | Op2 (Lambda, _, _, _, Cst (False, _, _)) => true
+  | Op2 (oper, _, _, u1, _) =>
     if oper = Apply then
       case u1 of
         ConstName (s, _, _) =>
@@ -661,7 +662,6 @@
       | _ => false
     else
       false
-  | Op2 (Lambda, _, _, _, Cst (False, _, _)) => true
   | _ => false
 
 fun rep_for_abs_fun scope T =