--- a/src/HOL/Induct/Tree.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Induct/Tree.thy Thu Sep 11 19:32:36 2014 +0200
@@ -9,7 +9,7 @@
imports Main
begin
-datatype_new 'a tree =
+datatype 'a tree =
Atom 'a
| Branch "nat => 'a tree"
@@ -34,7 +34,7 @@
subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*}
-datatype_new brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
+datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
text{*Addition of ordinals*}
primrec add :: "[brouwer,brouwer] => brouwer"