diff -r 9ae285ce814e -r 08c3ef07cef7 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Fri May 16 08:38:23 2014 +0100
+++ b/Nominal/Nominal2_Base.thy	Mon May 19 11:19:48 2014 +0100
@@ -2167,7 +2167,8 @@
 proof -
   have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_of M})" by simp
   also have "... \<subseteq> (\<Union>x \<in> set_of M. supp x)" by auto
-  also have "... = supp (set_of M)" by (simp add: supp_of_finite_sets)
+  also have "... = supp (set_of M)"
+    by (simp add: supp_of_finite_sets)
   also have " ... \<subseteq> supp M" by (rule supp_set_of)
   finally show "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" .
 qed
@@ -2953,7 +2954,6 @@
 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm =>
   case term_of ctrm of @{term "HOL.Not"} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) =>
     let  
-
       fun first_is_neg lhs rhs [] = NONE
         | first_is_neg lhs rhs (thm::thms) =
           (case Thm.prop_of thm of
@@ -2976,8 +2976,6 @@
          |> map (simplify (put_simpset HOL_basic_ss  ctxt addsimps simp_thms))
          |> map HOLogic.conj_elims
          |> flat
-
-       
     in 
       case first_is_neg lhs rhs prems of
         SOME(thm) => SOME(thm RS @{thm Eq_TrueI})