--- a/Nominal-General/Nominal2_Supp.thy	Sun Jul 18 19:07:05 2010 +0100
+++ b/Nominal-General/Nominal2_Supp.thy	Mon Jul 19 07:49:10 2010 +0100
@@ -193,7 +193,7 @@
       assume "a \<noteq> b"
       hence "atom a \<sharp> b" by (simp add: fresh_at_base)
       with a3 have "atom a \<sharp> h b" 
-	by (rule fresh_fun_app)
+        by (rule fresh_fun_app)
       with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)"
         by (rule swap_fresh_fresh)
       from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h"
@@ -392,8 +392,8 @@
     moreover
     { assume "supp p \<noteq> {}"
       then obtain a where a0: "a \<in> supp p" by blast
-      then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a" using as
-	by (auto simp add: supp_atom supp_perm swap_atom)
+      then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a"
+        using as by (auto simp add: supp_atom supp_perm swap_atom)
       let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"
       have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)
       moreover
@@ -503,14 +503,12 @@
   shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
 proof -
   have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
-    apply(rule supp_finite_atom_set[symmetric])
-    apply(rule Union_of_fin_supp_sets[OF fin])
-    done
+    by (rule supp_finite_atom_set[symmetric])
+       (rule Union_of_fin_supp_sets[OF fin])
   also have "\<dots> \<subseteq> supp S"
-    apply(rule supp_subset_fresh)
-    apply(simp add: Union_fresh)
-    done
-  finally show ?thesis .
+    by (rule supp_subset_fresh)
+       (simp add: Union_fresh)
+  finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
 qed
 
 lemma supp_of_fin_sets: