renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)

--- a/src/Doc/Datatypes/Datatypes.thy	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Feb 17 13:31:42 2014 +0100
@@ -103,7 +103,7 @@
 
 \item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive
 Functions,'' describes how to specify recursive functions using
-@{command primrec_new}, \keyw{fun}, and \keyw{function}.
+@{command primrec}, \keyw{fun}, and \keyw{function}.
 
 \item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
 describes how to specify codatatypes using the @{command codatatype} command.
@@ -147,10 +147,9 @@
 \newcommand\authoremailiv{\texttt{tray{\color{white}NOSPAM}\kern-\wd\boxA{}tel@\allowbreak
 in.\allowbreak tum.\allowbreak de}}
 
-The commands @{command datatype_new} and @{command primrec_new} are expected to
-replace \keyw{datatype} and \keyw{primrec} in a future release. Authors of new
-theories are encouraged to use the new commands, and maintainers of older
-theories may want to consider upgrading.
+The command @{command datatype_new} is expected to replace \keyw{datatype} in a
+future release. Authors of new theories are encouraged to use the new commands,
+and maintainers of older theories may want to consider upgrading.
 
 Comments and bug reports concerning either the tool or this tutorial should be
 directed to the authors at \authoremaili, \authoremailii, \authoremailiii,
@@ -979,13 +978,13 @@
 type of the recursor, used by \keyw{primrec}. Recursion through functions was
 handled specially. In the new package, nested recursion (for functions and
 non-functions) is handled in a more modular fashion. The old-style recursor can
-be generated on demand using @{command primrec_new}, as explained in
+be generated on demand using @{command primrec}, as explained in
 Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
 new-style datatypes.
 
 \item \emph{Accordingly, the induction rule is different for nested recursive
 datatypes.} Again, the old-style induction rule can be generated on demand using
-@{command primrec_new}, as explained in
+@{command primrec}, as explained in
 Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
 new-style datatypes.
 
@@ -1025,11 +1024,11 @@
   \label{sec:defining-recursive-functions} *}
 
 text {*
-Recursive functions over datatypes can be specified using the @{command
-primrec_new} command, which supports primitive recursion, or using the more
-general \keyw{fun} and \keyw{function} commands. Here, the focus is on @{command
-primrec_new}; the other two commands are described in a separate tutorial
-\cite{isabelle-function}.
+Recursive functions over datatypes can be specified using the @{command primrec}
+command, which supports primitive recursion, or using the more general
+\keyw{fun} and \keyw{function} commands. Here, the focus is on
+@{command primrec}; the other two commands are described in a separate
+tutorial \cite{isabelle-function}.
 
 %%% TODO: partial_function
 *}
@@ -1053,25 +1052,25 @@
 each equation. For example:
 *}
 
-    primrec_new bool_of_trool :: "trool \<Rightarrow> bool" where
+    primrec bool_of_trool :: "trool \<Rightarrow> bool" where
       "bool_of_trool Faalse \<longleftrightarrow> False" |
       "bool_of_trool Truue \<longleftrightarrow> True"
 
 text {* \blankline *}
 
-    primrec_new the_list :: "'a option \<Rightarrow> 'a list" where
+    primrec the_list :: "'a option \<Rightarrow> 'a list" where
       "the_list None = []" |
       "the_list (Some a) = [a]"
 
 text {* \blankline *}
 
-    primrec_new the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
+    primrec the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
       "the_default d None = d" |
       "the_default _ (Some a) = a"
 
 text {* \blankline *}
 
-    primrec_new mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where
+    primrec mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where
       "mirrror (Triple a b c) = Triple c b a"
 
 text {*
@@ -1091,13 +1090,13 @@
 allowed on the right-hand side:
 *}
 
-    primrec_new replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
+    primrec replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
       "replicate Zero _ = []" |
       "replicate (Suc n) x = x # replicate n x"
 
 text {* \blankline *}
 
-    primrec_new at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
+    primrec at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
       "at (x # xs) j =
          (case j of
             Zero \<Rightarrow> x
@@ -1105,7 +1104,7 @@
 
 text {* \blankline *}
 
-    primrec_new (*<*)(in early) (*>*)tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
+    primrec (*<*)(in early) (*>*)tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
       "tfold _ (TNil y) = y" |
       "tfold f (TCons x xs) = f x (tfold f xs)"
 
@@ -1149,7 +1148,7 @@
 is straightforward:
 *}
 
-    primrec_new
+    primrec
       nat_of_even_nat :: "even_nat \<Rightarrow> nat" and
       nat_of_odd_nat :: "odd_nat \<Rightarrow> nat"
     where
@@ -1159,7 +1158,7 @@
 
 text {* \blankline *}
 
-    primrec_new
+    primrec
       eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
       eval\<^sub>t :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) trm \<Rightarrow> int" and
       eval\<^sub>f :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) fct \<Rightarrow> int"
@@ -1199,7 +1198,7 @@
 (*<*)
     datatype_new 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f (lbl\<^sub>f\<^sub>f: 'a) (sub\<^sub>f\<^sub>f: "'a tree\<^sub>f\<^sub>f list")
 (*>*)
-    primrec_new at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" where
+    primrec at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" where
       "at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
          (case js of
             [] \<Rightarrow> a
@@ -1212,7 +1211,7 @@
 map function @{const map_option}:
 *}
 
-    primrec_new (*<*)(in early) (*>*)sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
+    primrec (*<*)(in early) (*>*)sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
       "sum_btree (BNode a lt rt) =
          a + the_default 0 (map_option sum_btree lt) +
            the_default 0 (map_option sum_btree rt)"
@@ -1224,7 +1223,7 @@
 (@{text \<Rightarrow>}) is simply composition (@{text "op \<circ>"}):
 *}
 
-    primrec_new (*<*)(in early) (*>*)relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
+    primrec (*<*)(in early) (*>*)relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
       "relabel_ft f (FTLeaf x) = FTLeaf (f x)" |
       "relabel_ft f (FTNode g) = FTNode (relabel_ft f \<circ> g)"
 
@@ -1235,13 +1234,13 @@
 For example:
 *}
 
-    primrec_new relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
+    primrec relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
       "relabel_ft f (FTLeaf x) = FTLeaf (f x)" |
       "relabel_ft f (FTNode g) = FTNode (\<lambda>x. relabel_ft f (g x))"
 
 text {* \blankline *}
 
-    primrec_new subtree_ft :: "'a \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
+    primrec subtree_ft :: "'a \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
       "subtree_ft x (FTNode g) = g x"
 
 text {*
@@ -1255,19 +1254,19 @@
 
 text {* \blankline *}
 
-    primrec_new (*<*)(in early) (*>*)relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
+    primrec (*<*)(in early) (*>*)relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
       "relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)" |
       "relabel_ft2 f (FTNode2 g) = FTNode2 (op \<circ> (op \<circ> (relabel_ft2 f)) g)"
 
 text {* \blankline *}
 
-    primrec_new relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
+    primrec relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
       "relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)" |
       "relabel_ft2 f (FTNode2 g) = FTNode2 (\<lambda>x y. relabel_ft2 f (g x y))"
 
 text {* \blankline *}
 
-    primrec_new subtree_ft2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
+    primrec subtree_ft2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
       "subtree_ft2 x y (FTNode2 g) = g x y"
 
 
@@ -1285,7 +1284,7 @@
 datatypes. For example:
 *}
 
-    primrec_new
+    primrec
       at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" and
       ats\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f list \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> 'a"
     where
@@ -1310,7 +1309,7 @@
 Here is a second example:
 *}
 
-    primrec_new
+    primrec
       sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" and
       sum_btree_option :: "'a btree option \<Rightarrow> 'a"
     where
@@ -1330,7 +1329,7 @@
 %
 %  * there's no hard-and-fast rule of when to use one or the other,
 %    just like there's no rule when to use fold and when to use
-%    primrec_new
+%    primrec
 %
 %  * higher-order approach, considering nesting as nesting, is more
 %    compositional -- e.g. we saw how we could reuse an existing polymorphic
@@ -1361,11 +1360,11 @@
 
 text {*
 \begin{matharray}{rcl}
-  @{command_def "primrec_new"} & : & @{text "local_theory \<rightarrow> local_theory"}
+  @{command_def "primrec"} & : & @{text "local_theory \<rightarrow> local_theory"}
 \end{matharray}
 
 @{rail \<open>
-  @@{command primrec_new} target? fixes \<newline> @'where' (@{syntax pr_equation} + '|')
+  @@{command primrec} target? fixes \<newline> @'where' (@{syntax pr_equation} + '|')
   ;
   @{syntax_def pr_equation}: thmdecl? prop
 \<close>}
@@ -1373,8 +1372,8 @@
 \medskip
 
 \noindent
-The @{command primrec_new} command introduces a set of mutually recursive
-functions over datatypes.
+The @{command primrec} command introduces a set of mutually recursive functions
+over datatypes.
 
 The syntactic entity \synt{target} can be used to specify a local context,
 \synt{fixes} denotes a list of names with optional type signatures,
@@ -1455,7 +1454,7 @@
     overloading
       termi\<^sub>0 \<equiv> "termi\<^sub>0 \<Colon> ('a, 'b) tlist \<Rightarrow> 'b"
     begin
-    primrec_new termi\<^sub>0 :: "('a, 'b) tlist \<Rightarrow> 'b" where
+    primrec termi\<^sub>0 :: "('a, 'b) tlist \<Rightarrow> 'b" where
       "termi\<^sub>0 (TNil y) = y" |
       "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"
     end
@@ -1470,9 +1469,10 @@
   \label{ssec:primrec-compatibility-issues} *}
 
 text {*
-The command @{command primrec_new} has been designed to be highly compatible
-with the old \keyw{primrec}, to ease migration. There is nonetheless at least
-one incompatibility that may arise when porting to the new package:
+The command @{command primrec}'s behavior on new-style datatypes has been
+designed to be highly compatible with that for old-style datatypes, to ease
+migration. There is nonetheless at least one incompatibility that may arise when
+porting to the new package:
 
 \begin{itemize}
 \setlength{\itemsep}{0pt}

--- a/src/HOL/BNF_Examples/Lambda_Term.thy	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/BNF_Examples/Lambda_Term.thy	Mon Feb 17 13:31:42 2014 +0100
@@ -23,13 +23,13 @@
 
 subsection {* Example: The set of all variables varsOf and free variables fvarsOf of a term *}
 
-primrec_new varsOf :: "'a trm \<Rightarrow> 'a set" where
+primrec varsOf :: "'a trm \<Rightarrow> 'a set" where
   "varsOf (Var a) = {a}"
 | "varsOf (App f x) = varsOf f \<union> varsOf x"
 | "varsOf (Lam x b) = {x} \<union> varsOf b"
 | "varsOf (Lt F t) = varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fimage (map_pair id varsOf) F})"
 
-primrec_new fvarsOf :: "'a trm \<Rightarrow> 'a set" where
+primrec fvarsOf :: "'a trm \<Rightarrow> 'a set" where
   "fvarsOf (Var x) = {x}"
 | "fvarsOf (App t1 t2) = fvarsOf t1 \<union> fvarsOf t2"
 | "fvarsOf (Lam x t) = fvarsOf t - {x}"

--- a/src/HOL/BNF_Examples/ListF.thy	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/BNF_Examples/ListF.thy	Mon Feb 17 13:31:42 2014 +0100
@@ -19,11 +19,11 @@
 definition Singll ("[[_]]") where
   [simp]: "Singll a \<equiv> Conss a NilF"
 
-primrec_new appendd (infixr "@@" 65) where
+primrec appendd (infixr "@@" 65) where
   "NilF @@ ys = ys"
 | "Conss x xs @@ ys = Conss x (xs @@ ys)"
 
-primrec_new lrev where
+primrec lrev where
   "lrev NilF = NilF"
 | "lrev (Conss y ys) = lrev ys @@ [[y]]"
 
@@ -46,7 +46,7 @@
 lemma lrev_lrev[simp]: "lrev (lrev xs) = xs"
   by (induct xs) auto
 
-primrec_new lengthh where
+primrec lengthh where
   "lengthh NilF = 0"
 | "lengthh (Conss x xs) = Suc (lengthh xs)"
 

--- a/src/HOL/BNF_Examples/Misc_Primrec.thy	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/BNF_Examples/Misc_Primrec.thy	Mon Feb 17 13:31:42 2014 +0100
@@ -11,49 +11,49 @@
 imports Misc_Datatype
 begin
 
-primrec_new nat_of_simple :: "simple \<Rightarrow> nat" where
+primrec nat_of_simple :: "simple \<Rightarrow> nat" where
   "nat_of_simple X1 = 1" |
   "nat_of_simple X2 = 2" |
   "nat_of_simple X3 = 3" |
   "nat_of_simple X4 = 4"
 
-primrec_new simple_of_simple' :: "simple' \<Rightarrow> simple" where
+primrec simple_of_simple' :: "simple' \<Rightarrow> simple" where
   "simple_of_simple' (X1' _) = X1" |
   "simple_of_simple' (X2' _) = X2" |
   "simple_of_simple' (X3' _) = X3" |
   "simple_of_simple' (X4' _) = X4"
 
-primrec_new inc_simple'' :: "nat \<Rightarrow> simple'' \<Rightarrow> simple''" where
+primrec inc_simple'' :: "nat \<Rightarrow> simple'' \<Rightarrow> simple''" where
   "inc_simple'' k (X1'' n i) = X1'' (n + k) (i + int k)" |
   "inc_simple'' _ X2'' = X2''"
 
-primrec_new myapp :: "'a mylist \<Rightarrow> 'a mylist \<Rightarrow> 'a mylist" where
+primrec myapp :: "'a mylist \<Rightarrow> 'a mylist \<Rightarrow> 'a mylist" where
   "myapp MyNil ys = ys" |
   "myapp (MyCons x xs) ys = MyCons x (myapp xs ys)"
 
-primrec_new myrev :: "'a mylist \<Rightarrow> 'a mylist" where
+primrec myrev :: "'a mylist \<Rightarrow> 'a mylist" where
   "myrev MyNil = MyNil" |
   "myrev (MyCons x xs) = myapp (myrev xs) (MyCons x MyNil)"
 
-primrec_new shuffle_sp :: "('a, 'b, 'c, 'd) some_passive \<Rightarrow> ('d, 'a, 'b, 'c) some_passive" where
+primrec shuffle_sp :: "('a, 'b, 'c, 'd) some_passive \<Rightarrow> ('d, 'a, 'b, 'c) some_passive" where
   "shuffle_sp (SP1 sp) = SP1 (shuffle_sp sp)" |
   "shuffle_sp (SP2 a) = SP3 a" |
   "shuffle_sp (SP3 b) = SP4 b" |
   "shuffle_sp (SP4 c) = SP5 c" |
   "shuffle_sp (SP5 d) = SP2 d"
 
-primrec_new
+primrec
   hf_size :: "hfset \<Rightarrow> nat"
 where
   "hf_size (HFset X) = 1 + setsum id (fset (fimage hf_size X))"
 
-primrec_new rename_lam :: "(string \<Rightarrow> string) \<Rightarrow> lambda \<Rightarrow> lambda" where
+primrec rename_lam :: "(string \<Rightarrow> string) \<Rightarrow> lambda \<Rightarrow> lambda" where
   "rename_lam f (Var s) = Var (f s)" |
   "rename_lam f (App l l') = App (rename_lam f l) (rename_lam f l')" |
   "rename_lam f (Abs s l) = Abs (f s) (rename_lam f l)" |
   "rename_lam f (Let SL l) = Let (fimage (map_pair f (rename_lam f)) SL) (rename_lam f l)"
 
-primrec_new
+primrec
   sum_i1 :: "('a\<Colon>{zero,plus}) I1 \<Rightarrow> 'a" and
   sum_i2 :: "'a I2 \<Rightarrow> 'a"
 where
@@ -62,18 +62,18 @@
   "sum_i2 I21 = 0" |
   "sum_i2 (I22 i j) = sum_i1 i + sum_i2 j"
 
-primrec_new forest_of_mylist :: "'a tree mylist \<Rightarrow> 'a forest" where
+primrec forest_of_mylist :: "'a tree mylist \<Rightarrow> 'a forest" where
   "forest_of_mylist MyNil = FNil" |
   "forest_of_mylist (MyCons t ts) = FCons t (forest_of_mylist ts)"
 
-primrec_new mylist_of_forest :: "'a forest \<Rightarrow> 'a tree mylist" where
+primrec mylist_of_forest :: "'a forest \<Rightarrow> 'a tree mylist" where
   "mylist_of_forest FNil = MyNil" |
   "mylist_of_forest (FCons t ts) = MyCons t (mylist_of_forest ts)"
 
 definition frev :: "'a forest \<Rightarrow> 'a forest" where
   "frev = forest_of_mylist \<circ> myrev \<circ> mylist_of_forest"
 
-primrec_new
+primrec
   mirror_tree :: "'a tree \<Rightarrow> 'a tree" and
   mirror_forest :: "'a forest \<Rightarrow> 'a forest"
 where
@@ -82,7 +82,7 @@
   "mirror_forest FNil = FNil" |
   "mirror_forest (FCons t ts) = frev (FCons (mirror_tree t) (mirror_forest ts))"
 
-primrec_new
+primrec
   mylist_of_tree' :: "'a tree' \<Rightarrow> 'a mylist" and
   mylist_of_branch :: "'a branch \<Rightarrow> 'a mylist"
 where
@@ -90,7 +90,7 @@
   "mylist_of_tree' (TNode' b b') = myapp (mylist_of_branch b) (mylist_of_branch b')" |
   "mylist_of_branch (Branch x t) = MyCons x (mylist_of_tree' t)"
 
-primrec_new
+primrec
   id_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and
   id_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and
   id_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist"
@@ -101,7 +101,7 @@
   "id_trees2 MyNil = MyNil" |
   "id_trees2 (MyCons t ts) = MyCons (id_tree t) (id_trees2 ts)"
 
-primrec_new
+primrec
   is_ground_exp :: "('a, 'b) exp \<Rightarrow> bool" and
   is_ground_trm :: "('a, 'b) trm \<Rightarrow> bool" and
   is_ground_factor :: "('a, 'b) factor \<Rightarrow> bool"
@@ -114,11 +114,11 @@
   "is_ground_factor (V _) \<longleftrightarrow> False" |
   "is_ground_factor (Paren e) \<longleftrightarrow> is_ground_exp e"
 
-primrec_new map_ftreeA :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
+primrec map_ftreeA :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
   "map_ftreeA f (FTLeaf x) = FTLeaf (f x)" |
   "map_ftreeA f (FTNode g) = FTNode (map_ftreeA f \<circ> g)"
 
-primrec_new map_ftreeB :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ftree \<Rightarrow> 'b ftree" where
+primrec map_ftreeB :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ftree \<Rightarrow> 'b ftree" where
   "map_ftreeB f (FTLeaf x) = FTLeaf (f x)" |
   "map_ftreeB f (FTNode g) = FTNode (map_ftreeB f \<circ> g \<circ> the_inv f)"
 

--- a/src/HOL/BNF_Examples/Stream_Processor.thy	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/BNF_Examples/Stream_Processor.thy	Mon Feb 17 13:31:42 2014 +0100
@@ -17,7 +17,7 @@
 datatype_new ('a, 'b, 'c) sp\<^sub>\<mu> = Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" | Put "'b" "'c"
 codatatype ('a, 'b) sp\<^sub>\<nu> = In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>")
 
-primrec_new run\<^sub>\<mu> :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> ('b \<times> 'c) \<times> 'a stream" where
+primrec run\<^sub>\<mu> :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> ('b \<times> 'c) \<times> 'a stream" where
   "run\<^sub>\<mu> (Get f) s = run\<^sub>\<mu> (f (shd s)) (stl s)"
 | "run\<^sub>\<mu> (Put b sp) s = ((b, sp), s)"
 
@@ -81,13 +81,13 @@
   qed
 qed
 
-text {* Alternative definition of composition using primrec_new instead of function *}
+text {* Alternative definition of composition using primrec instead of function *}
 
-primrec_new sp\<^sub>\<mu>_comp2R  where
+primrec sp\<^sub>\<mu>_comp2R  where
   "sp\<^sub>\<mu>_comp2R f (Put b sp) = f b (out sp)"
 | "sp\<^sub>\<mu>_comp2R f (Get h) = Get (sp\<^sub>\<mu>_comp2R f o h)"
 
-primrec_new sp\<^sub>\<mu>_comp2 (infixl "o\<^sup>*\<^sub>\<mu>" 65) where
+primrec sp\<^sub>\<mu>_comp2 (infixl "o\<^sup>*\<^sub>\<mu>" 65) where
   "Put b sp o\<^sup>*\<^sub>\<mu> fsp = Put b (sp, In fsp)"
 | "Get f o\<^sup>*\<^sub>\<mu> fsp = sp\<^sub>\<mu>_comp2R (op o\<^sup>*\<^sub>\<mu> o f) fsp"
 
@@ -177,7 +177,7 @@
 
 (* Definition of run for an arbitrary final coalgebra as codomain: *)
 
-primrec_new
+primrec
   runF\<^sub>\<mu> :: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> (('b, ('a, 'b) spF\<^sub>\<nu>) F) \<times> 'a stream" 
 where
   "runF\<^sub>\<mu> (GetF f) s = (runF\<^sub>\<mu> o f) (shd s) (stl s)"

--- a/src/HOL/BNF_LFP.thy	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/BNF_LFP.thy	Mon Feb 17 13:31:42 2014 +0100
@@ -13,8 +13,7 @@
 imports BNF_FP_Base
 keywords
   "datatype_new" :: thy_decl and
-  "datatype_new_compat" :: thy_decl and
-  "primrec_new" :: thy_decl
+  "datatype_new_compat" :: thy_decl
 begin
 
 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"

--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Feb 17 13:31:42 2014 +0100
@@ -355,7 +355,7 @@
       end;
 
     (* These results are half broken. This is deliberate. We care only about those fields that are
-       used by "primrec_new", "primcorecursive", and "datatype_new_compat". *)
+       used by "primrec", "primcorecursive", and "datatype_new_compat". *)
     val fp_res =
       ({Ts = fpTs,
         bnfs = steal #bnfs,

--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Feb 17 13:31:42 2014 +0100
@@ -560,9 +560,9 @@
   end
   handle PRIMREC (str, eqns) =>
          if null eqns then
-           error ("primrec_new error:\n  " ^ str)
+           error ("primrec error:\n  " ^ str)
          else
-           error ("primrec_new error:\n  " ^ str ^ "\nin\n  " ^
+           error ("primrec error:\n  " ^ str ^ "\nin\n  " ^
              space_implode "\n  " (map (quote o Syntax.string_of_term lthy) eqns));
 
 fun gen_primrec old_primrec prep_spec (raw_fixes : (binding * 'a option * mixfix) list) raw_spec
@@ -612,7 +612,7 @@
     val simpss' = burrow (Proof_Context.export lthy' lthy) simpss;
   in ((ts, simpss'), Local_Theory.exit_global lthy') end;
 
-val _ = Outer_Syntax.local_theory @{command_spec "primrec_new"}
+val _ = Outer_Syntax.local_theory @{command_spec "primrec"}
   "define primitive recursive functions"
   (Parse.fixes -- Parse_Spec.where_alt_specs >> (snd oo uncurry add_primrec_cmd));