--- a/Nominal/Nominal2_Base_Exec.thy	Thu May 24 10:17:32 2012 +0200
+++ b/Nominal/Nominal2_Base_Exec.thy	Fri May 25 15:46:48 2012 +0100
@@ -2735,7 +2735,7 @@
              _ $ (@{term "HOL.Not"} $ (Const ("HOL.eq", _) $ l $ r)) =>
                (if l = lhs andalso r = rhs then SOME(thm)
                 else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym})
-                else NONE)
+                else first_is_neg lhs rhs thms)
            | _ => first_is_neg lhs rhs thms)
 
     val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff}