diff -r 040519ec99e9 -r b52e8651591f Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/Ex/Lambda.thy	Thu Mar 13 09:21:31 2014 +0000
@@ -593,7 +593,7 @@
   "transdb (Var x) l = vindex l x 0"
 | "transdb (App t1 t2) xs = 
       Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))"
-| "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))"
+| "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map_option DBLam (transdb t (x # xs))"
   apply(simp add: eqvt_def transdb_graph_aux_def)
   apply(rule TrueI)
   apply (case_tac x)