# HG changeset patch
# User blanchet
# Date 1325611997 -3600
# Node ID b58591c75f0dd0f3e33ef7fd89dd4795141d2ed7
# Parent  65bde43e829c3e0ca5c8a168f4fba627debada75
fixed spurious catch-all patterns

diff -r 65bde43e829c -r b58591c75f0d src/HOL/Tools/Nitpick/nitrox.ML
--- a/src/HOL/Tools/Nitpick/nitrox.ML	Tue Jan 03 13:06:03 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitrox.ML	Tue Jan 03 18:33:17 2012 +0100
@@ -91,9 +91,7 @@
           AAnd => HOLogic.mk_conj
         | AOr => HOLogic.mk_disj
         | AImplies => HOLogic.mk_imp
-        | AIf => HOLogic.mk_imp o swap
         | AIff => HOLogic.mk_eq
-        | ANotIff => HOLogic.mk_not o HOLogic.mk_eq
         | ANot => raise Fail "binary \"ANot\"")
   | AConn _ => raise Fail "malformed AConn"
   | AAtom u => hol_term_from_fo_term boolT u