diff -r c95afd0dc594 -r 5e74bd87bcda Nominal/Ex/SFT/LambdaTerms.thy
--- a/Nominal/Ex/SFT/LambdaTerms.thy	Wed Dec 21 15:43:58 2011 +0900
+++ b/Nominal/Ex/SFT/LambdaTerms.thy	Wed Dec 21 15:47:42 2011 +0900
@@ -5,25 +5,25 @@
 lemma [simp]: "supp x = {} \<Longrightarrow> y \<sharp> x"
   unfolding fresh_def by blast
 
-atom_decl var
+atom_decl name
 
 nominal_datatype lam =
-  Var "var"
+  Var "name"
 | App "lam" "lam"
-| Lam x::"var" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
+| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
 notation
   App (infixl "\<cdot>" 98) and
   Lam ("\<integral> _. _" [97, 97] 99)
 
 nominal_primrec
-  subst :: "lam \<Rightarrow> var \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
 where
   "(Var x)[y ::= s] = (if x = y then s else (Var x))"
 | "(t1 \<cdot> t2)[y ::= s] = (t1[y ::= s]) \<cdot> (t2[y ::= s])"
 | "atom x \<sharp> (y, s) \<Longrightarrow> (\<integral>x. t)[y ::= s] = \<integral>x.(t[y ::= s])"
 proof auto
-  fix a b :: lam and aa :: var and P
+  fix a b :: lam and aa :: name and P
   assume "\<And>x y s. a = Var x \<and> aa = y \<and> b = s \<Longrightarrow> P"
     "\<And>t1 t2 y s. a = t1 \<cdot> t2 \<and> aa = y \<and> b = s \<Longrightarrow> P"
     "\<And>x y s t. \<lbrakk>atom x \<sharp> (y, s); a = \<integral> x. t \<and> aa = y \<and> b = s\<rbrakk> \<Longrightarrow> P"
@@ -31,7 +31,7 @@
     by (rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
        (blast, blast, simp add: fresh_star_def)
 next
-  fix x :: var and t and xa :: var and ya sa ta
+  fix x :: name and t and xa :: name and ya sa ta
   assume *: "eqvt_at subst_sumC (t, ya, sa)"
     "atom x \<sharp> (ya, sa)" "atom xa \<sharp> (ya, sa)"
     "[[atom x]]lst. t = [[atom xa]]lst. ta"