src/HOL/Nominal/Examples/Pattern.thy

       by (simp add: btrm.inject alpha)
     then show ?thesis
     proof
       assume "x = x' \<and> t = u"
       with PVar PVar' have "PVar x T = ([]::name prm) \<bullet> q \<and>
-	t = ([]::name prm) \<bullet> u \<and>
-	set ([]::name prm) \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
+        t = ([]::name prm) \<bullet> u \<and>
+        set ([]::name prm) \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
           (supp (PVar x T) \<union> supp q)" by simp
       then show ?thesis ..
     next
       assume "x \<noteq> x' \<and> t = [(x, x')] \<bullet> u \<and> x \<sharp> u"
       with PVar PVar' have "PVar x T = [(x, x')] \<bullet> q \<and>
-	t = [(x, x')] \<bullet> u \<and>
-	set [(x, x')] \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
+        t = [(x, x')] \<bullet> u \<and>
+        set [(x, x')] \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
           (supp (PVar x T) \<union> supp q)"
-	by (simp add: perm_swap swap_simps supp_atm perm_type)
+        by (simp add: perm_swap swap_simps supp_atm perm_type)
       then show ?thesis ..
     qed
   next
     case (PTuple p\<^isub>1 p\<^isub>2)
     with PVar have "ty_size (pat_type p\<^isub>1) < ty_size T" by simp