--- a/Nominal/Ex/SubstNoFcb.thy	Thu Mar 29 10:37:41 2012 +0200
+++ b/Nominal/Ex/SubstNoFcb.thy	Fri Mar 30 07:15:24 2012 +0200
@@ -65,7 +65,7 @@
   shows "\<lbrakk>a \<sharp> x; a \<sharp> y; a \<sharp> z\<rbrakk> \<Longrightarrow> a \<sharp> f x y z"
   using fresh_fun_eqvt_app[OF e] fresh_fun_app by (metis (lifting, full_types))
 
-lemma
+lemma substr_simps:
   "substr (Var x) y s = (if x = y then s else (Var x))"
   "substr (App t1 t2) y s = App (substr t1 y s) (substr t2 y s)"
   "atom x \<sharp> (y, s) \<Longrightarrow> substr (Lam [x]. t) y s = Lam [x]. (substr t y s)"