--- a/Nominal/Ex/Lambda.thy	Tue May 22 14:55:58 2012 +0200
+++ b/Nominal/Ex/Lambda.thy	Wed May 23 23:57:27 2012 +0100
@@ -7,6 +7,7 @@
 
 atom_decl name
 
+
 ML {* trace := true *}
 
 nominal_datatype lam =

--- a/Nominal/Nominal2_Base.thy	Tue May 22 14:55:58 2012 +0200
+++ b/Nominal/Nominal2_Base.thy	Wed May 23 23:57:27 2012 +0100
@@ -2187,6 +2187,7 @@
 end
 *}
 
+
 text {* The fresh-star generalisation of fresh is used in strong
   induction principles. *}
 
@@ -2810,6 +2811,40 @@
   shows "as \<sharp>* atom b \<longleftrightarrow> as \<sharp>* b"
   by (simp add: fresh_star_def fresh_atom_at_base)
 
+lemma if_fresh_at_base [simp]:
+  shows "atom a \<sharp> x \<Longrightarrow> P (if a = x then t else s) = P s"
+  and   "atom a \<sharp> x \<Longrightarrow> P (if x = a then t else s) = P s"
+by (simp_all add: fresh_at_base)
+
+simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ss => fn ctrm =>
+  let
+    fun first_is_neg lhs rhs [] = NONE
+      | first_is_neg lhs rhs (thm::thms) =
+          (case Thm.prop_of thm of
+             _ $ (@{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)  
+           | _ => first_is_neg lhs rhs thms)
+
+    val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff}
+    val prems = Simplifier.prems_of ss
+      |> filter (fn thm => case Thm.prop_of thm of                    
+           _ $ (Const (@{const_name fresh}, _) $ _ $ _) => true | _ => false)
+      |> map (simplify (HOL_basic_ss addsimps simp_thms))
+      |> map HOLogic.conj_elims
+      |> flat
+  in 
+    case term_of ctrm of
+      @{term "HOL.Not"} $ (Const ("HOL.eq", _) $ lhs $ rhs) => 
+         (case first_is_neg lhs rhs prems of
+            SOME(thm) => SOME(thm RS @{thm Eq_TrueI})
+          | NONE => NONE)
+    | _ => NONE
+  end
+*}
+
+
 instance at_base < fs
 proof qed (simp add: supp_at_base)
 
@@ -3123,7 +3158,7 @@
   fix x y
   assume x: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
   assume y: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = y"
-  from a x y show "x = y"
+  from a x y show "x = y" 
     by (auto simp add: fresh_Pair)
 qed