diff -r c95afd0dc594 -r 5e74bd87bcda Nominal/Ex/SFT/Utils.thy
--- a/Nominal/Ex/SFT/Utils.thy	Wed Dec 21 15:43:58 2011 +0900
+++ b/Nominal/Ex/SFT/Utils.thy	Wed Dec 21 15:47:42 2011 +0900
@@ -12,7 +12,7 @@
       and su: "\<And>x. atom x \<sharp> A \<Longrightarrow> F (V x) [x ::= A] = F A"
   shows "L \<cdot> A \<approx> F A"
 proof -
-  obtain x :: var where a: "atom x \<sharp> A" using obtain_fresh by blast
+  obtain x :: name where a: "atom x \<sharp> A" using obtain_fresh by blast
   show ?thesis
     by (simp add: leq[of x], rule b3, rule bI, simp add: su b1 a)
 qed
@@ -23,9 +23,9 @@
        x \<noteq> y \<Longrightarrow> F (V x) (V y) [x ::= A] [y ::= B] = F A B"
   shows "L \<cdot> A \<cdot> B \<approx> F A B"
 proof -
-  obtain x :: var where a: "atom x \<sharp> (A, B)" using obtain_fresh by blast
-  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 x :: name where a: "atom x \<sharp> (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> y" "x \<noteq> z" "y \<noteq> z"
     using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+
   have ** : "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x"
@@ -51,9 +51,9 @@
       ((F (V x) (V y) (V z))[x ::= A] [y ::= B] [z ::= C] = F A B C)"
   shows "L \<cdot> A \<cdot> B \<cdot> C \<approx> F A B C"
 proof -
-  obtain x :: var where a: "atom x \<sharp> (A, B, C)" using obtain_fresh by blast
-  obtain y :: var where b: "atom y \<sharp> (x, A, B, C)" using obtain_fresh by blast
-  obtain z :: var where c: "atom z \<sharp> (x, y, A, B, C)" using obtain_fresh by blast
+  obtain x :: name where a: "atom x \<sharp> (A, B, C)" using obtain_fresh by blast
+  obtain y :: name where b: "atom y \<sharp> (x, A, B, C)" using obtain_fresh by blast
+  obtain z :: name where c: "atom z \<sharp> (x, y, A, B, C)" using obtain_fresh by blast
   have *: "x \<noteq> y" "y \<noteq> z" "z \<noteq> x"
     using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+
   have ** : "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x"
@@ -72,14 +72,14 @@
     done
   qed
 
-definition cn :: "nat \<Rightarrow> var" where "cn n \<equiv> Abs_var (Atom (Sort ''LambdaTerms.var'' []) n)"
+definition cn :: "nat \<Rightarrow> name" where "cn n \<equiv> Abs_name (Atom (Sort ''LambdaTerms.name'' []) n)"
 
 lemma cnd[simp]: "m \<noteq> n \<Longrightarrow> cn m \<noteq> cn n"
-  unfolding cn_def using Abs_var_inject by simp
+  unfolding cn_def using Abs_name_inject by simp
 
-definition cx :: var where "cx \<equiv> cn 0"
-definition cy :: var where "cy \<equiv> cn 1"
-definition cz :: var where "cz \<equiv> cn 2"
+definition cx :: name where "cx \<equiv> cn 0"
+definition cy :: name where "cy \<equiv> cn 1"
+definition cz :: name where "cz \<equiv> cn 2"
 
 lemma cx_cy_cz[simp]:
   "cx \<noteq> cy" "cx \<noteq> cz" "cz \<noteq> cy"