--- a/src/HOL/Nominal/Examples/Pattern.thy Wed Oct 28 00:23:39 2009 +0100
+++ b/src/HOL/Nominal/Examples/Pattern.thy Wed Oct 28 00:24:38 2009 +0100
@@ -669,17 +669,17 @@
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