diff -r 08c3ef07cef7 -r 5ebd327ffb96 Nominal/Ex/LamTest.thy
--- a/Nominal/Ex/LamTest.thy	Mon May 19 11:19:48 2014 +0100
+++ b/Nominal/Ex/LamTest.thy	Mon May 19 12:45:26 2014 +0100
@@ -1507,7 +1507,7 @@
 (* outer syntax *)
 
 val _ =
-  Outer_Syntax.local_theory_to_proof "nominal_primrec" "define recursive functions for nominal types"
+  Outer_Syntax.local_theory_to_proof "nominal_function" "define recursive functions for nominal types"
   Keyword.thy_goal
   (function_parser default_config
      >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
@@ -1545,7 +1545,7 @@
   shows "(a \<rightleftharpoons> c) \<bullet> x = (b \<rightleftharpoons> c) \<bullet> y"
 using assms by (simp add: swap_fresh_fresh)
 
-nominal_primrec
+nominal_function
   depth :: "lam \<Rightarrow> nat"
 where
   "depth (Var x) = 1"
@@ -1566,7 +1566,7 @@
   shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
 by (induct xs) (auto)
 
-nominal_primrec 
+nominal_function 
   frees_lst :: "lam \<Rightarrow> atom list"
 where
   "frees_lst (Var x) = [atom x]"
@@ -1585,7 +1585,7 @@
 apply(clarify)
 oops
 
-nominal_primrec
+nominal_function
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
 where
   "(Var x)[y ::= s] = (if x=y then s else (Var x))"
@@ -1608,7 +1608,7 @@
 
 
 
-nominal_primrec
+nominal_function
   depth :: "lam \<Rightarrow> nat"
 where
   "depth (Var x) = 1"
@@ -1665,7 +1665,7 @@
   shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
 by (induct xs) (auto)
 
-nominal_primrec 
+nominal_function 
   frees_lst :: "lam \<Rightarrow> atom list"
 where
   "frees_lst (Var x) = [atom x]"
@@ -1687,7 +1687,7 @@
 apply(rule_tac p="p" in supp_perm_eq)
 oops
 
-nominal_primrec 
+nominal_function 
   frees :: "lam \<Rightarrow> name set"
 where
   "frees (Var x) = {x}"
@@ -1771,7 +1771,7 @@
 apply(simp add: set_eqvt)
 sorry
 
-nominal_primrec
+nominal_function
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
 where
   "(Var x)[y ::= s] = (if x=y then s else (Var x))"
@@ -1822,7 +1822,7 @@
 
 
 
-nominal_primrec
+nominal_function
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
 where
   "(Var x)[y ::= s] = (if x=y then s else (Var x))"
@@ -1874,7 +1874,7 @@
 done
 
 (* this should not work *)
-nominal_primrec 
+nominal_function 
   bnds :: "lam \<Rightarrow> name set"
 where
   "bnds (Var x) = {}"