diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/LetSimple2.thy
--- a/Nominal/Ex/LetSimple2.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LetSimple2.thy	Mon May 19 12:45:26 2014 +0100
@@ -111,7 +111,7 @@
 done
 
 
-nominal_primrec
+nominal_function
     height_trm :: "trm \<Rightarrow> nat"
 where
   "height_trm (Var x) = 1"
@@ -143,7 +143,7 @@
 termination by lexicographic_order
 *)
 
-nominal_primrec 
+nominal_function 
   subst_trm :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm"  ("_ [_ ::= _]" [90, 90, 90] 90) 
 where
   "(Var x)[y ::= s] = (if x = y then s else (Var x))"
@@ -197,7 +197,7 @@
 
 
 
-nominal_primrec 
+nominal_function 
 <<<<<<< variant A
  (invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True | Inr x2 \<Rightarrow> alpha_bn_preserve (height_assn2::assn \<Rightarrow> nat) x2")
 >>>>>>> variant B
@@ -334,7 +334,7 @@
 
 text {* works, but only because no recursion in as *}
 
-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}"
@@ -381,7 +381,7 @@
 done
 
 
-nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
+nominal_function (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
   subst_trm2 :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm"  ("_ [_ ::trm2= _]" [90, 90, 90] 90) and
   subst_assn2 :: "assn \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> assn"  ("_ [_ ::assn2= _]" [90, 90, 90] 90)
 where
@@ -488,4 +488,4 @@
 done
 
 
-end
\ No newline at end of file
+end