--- a/src/HOL/Nominal/Examples/Lam_Funs.thy Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/Nominal/Examples/Lam_Funs.thy Tue Aug 13 16:25:47 2013 +0200
@@ -79,7 +79,7 @@
psubst :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam" ("_<_>" [95,95] 105)
where
"\<theta><(Var x)> = (lookup \<theta> x)"
-| "\<theta><(App e\<^isub>1 e\<^isub>2)> = App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>)"
+| "\<theta><(App e\<^sub>1 e\<^sub>2)> = App (\<theta><e\<^sub>1>) (\<theta><e\<^sub>2>)"
| "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)"
apply(finite_guess)+
apply(rule TrueI)+