move equation up where it's not ignored
authorblanchet
Mon, 13 Sep 2010 20:15:04 +0200
changeset 39343 eac5f82eefb6
parent 39342 1a0e6f16a91b
child 39344 9de74cdcd833
move equation up where it's not ignored
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 =