# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1337957208 -3600
# Node ID 31372760c2fb2dc322d7075fb3e3c660cd9266d7
# Parent  52730e5ec8cb6a89890da34a144b2428211dc3ee
fixed bug in simproc (also in the exec-version)

diff -r 52730e5ec8cb -r 31372760c2fb Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Thu May 24 10:17:32 2012 +0200
+++ b/Nominal/Nominal2_Base.thy	Fri May 25 15:46:48 2012 +0100
@@ -2827,7 +2827,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}
diff -r 52730e5ec8cb -r 31372760c2fb Nominal/Nominal2_Base_Exec.thy
--- 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}