diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/LetSimple1.thy
--- a/Nominal/Ex/LetSimple1.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LetSimple1.thy	Mon May 19 12:45:26 2014 +0100
@@ -25,7 +25,7 @@
 thm trm.strong_exhaust
 thm trm.perm_bn_simps
 
-nominal_primrec
+nominal_function
     height_trm :: "trm \<Rightarrow> nat"
 where
   "height_trm (Var x) = 1"
@@ -51,7 +51,7 @@
   by lexicographic_order
 
 
-nominal_primrec (invariant "\<lambda>x (y::atom set). finite y")
+nominal_function (invariant "\<lambda>x (y::atom set). finite y")
   frees_set :: "trm \<Rightarrow> atom set"
 where
   "frees_set (Var x) = {atom x}"
@@ -79,7 +79,7 @@
   by lexicographic_order
 
 
-nominal_primrec
+nominal_function
   subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm"  ("_ [_ ::= _]" [90, 90, 90] 90)
 where
   "(Var x)[y ::= s] = (if x = y then s else (Var x))"
@@ -108,4 +108,4 @@
   by lexicographic_order
 
 
-end
\ No newline at end of file
+end