src/HOL/Induct/Tree.thy
changeset 58310 91ea607a34d8
parent 58249 180f1b3508ed
child 58889 5b7a9633cfa8
--- 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"