diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/LetRecFunNo.thy
--- a/Nominal/Ex/LetRecFunNo.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LetRecFunNo.thy	Mon May 19 12:45:26 2014 +0100
@@ -17,7 +17,7 @@
   "bn ANil = []"
 | "bn (ACons x t as) = (atom x) # (bn as)"
 
-nominal_primrec substrec where
+nominal_function substrec where
   "substrec fa fl fd y z (Var x) = (if (y = x) then z else (Var x))"
 | "substrec fa fl fd y z (App l r) = fa l r"
 | "(set (bn as) \<sharp>* (Let as t, y, z) \<and> (\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let as t = Let bs s \<longrightarrow> fl as t = fl bs s)) \<Longrightarrow>
@@ -55,7 +55,7 @@
   done
 termination (eqvt) by lexicographic_order
 
-nominal_primrec substarec :: "(name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn) \<Rightarrow> assn \<Rightarrow> assn" where
+nominal_function substarec :: "(name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn) \<Rightarrow> assn \<Rightarrow> assn" where
   "substarec fac ANil = ANil"
 | "substarec fac (ACons x t as) = fac x t as"
   unfolding eqvt_def substarec_graph_def