--- a/Nominal/Ex/Lambda.thy	Wed Jan 19 19:06:52 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Wed Jan 19 19:41:50 2011 +0100
@@ -213,7 +213,7 @@
   assumes a: "t1 \<longrightarrow>1 t2" "s1 \<longrightarrow>1 s2"
   shows "App (Lam [x]. t1) s1 \<longrightarrow>1 t2[ x ::= s2]"
 proof -
-  obtain y::"name" where fs: "atom y \<sharp> (x, t1, s1, t2, s2)" sorry
+  obtain y::"name" where fs: "atom y \<sharp> (x, t1, s1, t2, s2)" by (rule obtain_fresh)
   have "App (Lam [x]. t1) s1 = App (Lam [y]. ((y \<leftrightarrow> x) \<bullet> t1)) s1" using fs
     by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)
   also have "\<dots> \<longrightarrow>1 ((y \<leftrightarrow> x) \<bullet> t2)[y ::= s2]" using fs a by (auto simp add: One.eqvt)
@@ -223,8 +223,6 @@
 
 
 
-
-
 section {* Locally Nameless Terms *}
 
 nominal_datatype ln = 
@@ -250,7 +248,7 @@
 where
   "trans (Var x) xs = lookup xs 0 x"
 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
-| "atom x \<sharp> xs \<Longrightarrow> trans (Lam x t) xs = LNLam (trans t (x # xs))"
+| "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
 apply(case_tac x)
 apply(simp)
 apply(rule_tac y="a" and c="b" in lam.strong_exhaust)