diff -r c95afd0dc594 -r 5e74bd87bcda Nominal/Ex/SFT/Consts.thy
--- a/Nominal/Ex/SFT/Consts.thy	Wed Dec 21 15:43:58 2011 +0900
+++ b/Nominal/Ex/SFT/Consts.thy	Wed Dec 21 15:47:42 2011 +0900
@@ -84,7 +84,7 @@
     by (rule_tac y="x" and c="0 :: perm" in lam.strong_exhaust)
        (auto simp add: Abs1_eq_iff fresh_star_def)[3]
 next
-  fix x :: var and M and xa :: var and Ma
+  fix x :: name and M and xa :: name and Ma
   assume "[[atom x]]lst. M = [[atom xa]]lst. Ma"
     "eqvt_at Numeral_sumC M"
   then show "[[atom x]]lst. Numeral_sumC M = [[atom xa]]lst. Numeral_sumC Ma"
@@ -110,7 +110,7 @@
   "x \<sharp> \<lbrace>y\<rbrace> = x \<sharp> y"
   unfolding fresh_def by simp
 
-fun app_lst :: "var \<Rightarrow> lam list \<Rightarrow> lam" where
+fun app_lst :: "name \<Rightarrow> lam list \<Rightarrow> lam" where
   "app_lst n [] = Var n"
 | "app_lst n (h # t) = (app_lst n t) \<cdot> h"
 
@@ -134,7 +134,7 @@
   [simp del]: "atom x \<sharp> l \<Longrightarrow> \<guillemotleft>l\<guillemotright> = \<integral>x. (app_lst x (rev l))"
   unfolding eqvt_def Ltgt_graph_def
   apply (rule, perm_simp, rule, rule)
-  apply (rule_tac x="x" and ?'a="var" in obtain_fresh)
+  apply (rule_tac x="x" and ?'a="name" in obtain_fresh)
   apply (simp_all add: Abs1_eq_iff lam.fresh swap_fresh_fresh fresh_at_base)
   apply (simp add: eqvts swap_fresh_fresh)
   apply (case_tac "x = xa")
@@ -149,14 +149,14 @@
 lemma ltgt_eq_iff[simp]:
   "\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright> \<longleftrightarrow> M = N"
 proof auto
-  obtain x :: var where "atom x \<sharp> (M, N)" using obtain_fresh by auto
+  obtain x :: name where "atom x \<sharp> (M, N)" using obtain_fresh by auto
   then have *: "atom x \<sharp> M" "atom x \<sharp> N" using fresh_Pair by simp_all
   then show "(\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright>) \<Longrightarrow> (M = N)" by (simp add: Abs1_eq_iff app_lst_rev_eq_iff Ltgt.simps)
 qed
 
 lemma Ltgt1_app: "\<guillemotleft>[M]\<guillemotright> \<cdot> N \<approx> N \<cdot> M"
 proof -
-  obtain x :: var where "atom x \<sharp> (M, N)" using obtain_fresh by auto
+  obtain x :: name where "atom x \<sharp> (M, N)" using obtain_fresh by auto
   then have "atom x \<sharp> M" "atom x \<sharp> N" using fresh_Pair by simp_all
   then show ?thesis
   apply (subst Ltgt.simps)
@@ -167,7 +167,7 @@
 
 lemma Ltgt3_app: "\<guillemotleft>[M,N,P]\<guillemotright> \<cdot> R \<approx> R \<cdot> M \<cdot> N \<cdot> P"
 proof -
-  obtain x :: var where "atom x \<sharp> (M, N, P, R)" using obtain_fresh by auto
+  obtain x :: name where "atom x \<sharp> (M, N, P, R)" using obtain_fresh by auto
   then have *: "atom x \<sharp> (M,N,P)" "atom x \<sharp> R" using fresh_Pair by simp_all
   then have s: "Var x \<cdot> M \<cdot> N \<cdot> P [x ::= R] \<approx> R \<cdot> M \<cdot> N \<cdot> P" using b1 by simp
   show ?thesis using *
@@ -181,7 +181,7 @@
 lemma supp_ltgt[simp]:
   "supp \<guillemotleft>t\<guillemotright> = supp t"
 proof -
-  obtain x :: var where *:"atom x \<sharp> t" using obtain_fresh by auto
+  obtain x :: name where *:"atom x \<sharp> t" using obtain_fresh by auto
   show ?thesis using *
   by (simp_all add: Ltgt.simps lam.supp supp_at_base supp_Nil supp_app_lst supp_rev fresh_def)
 qed
@@ -194,7 +194,7 @@
 lemma Ltgt1_subst[simp]:
   "\<guillemotleft>[M]\<guillemotright> [y ::= A] = \<guillemotleft>[M [y ::= A]]\<guillemotright>"
 proof -
-  obtain x :: var where a: "atom x \<sharp> (M, A, y, M [y ::= A])" using obtain_fresh by blast
+  obtain x :: name where a: "atom x \<sharp> (M, A, y, M [y ::= A])" using obtain_fresh by blast
   have "x \<noteq> y" using a[simplified fresh_Pair fresh_at_base] by simp
   then show ?thesis
     apply (subst Ltgt.simps)
@@ -242,8 +242,8 @@
   assumes f: "atom x \<sharp> A" "atom x \<sharp> B" (* or A and B have empty support *)
   shows "F3 \<cdot> A \<cdot> B \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (B \<cdot> (A \<cdot> Var x))))"
 proof -
-  obtain y :: var where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast
-  obtain z :: var where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast
+  obtain y :: name where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast
+  obtain z :: name where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast
   have *: "x \<noteq> z" "x \<noteq> y" "y \<noteq> z"
     using b c by (simp_all add: fresh_Pair fresh_at_base) blast+
   have **: