diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Reflection_Examples.thy
--- a/src/HOL/ex/Reflection_Examples.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Reflection_Examples.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -46,7 +46,7 @@
 text {* Example 1 : Propositional formulae and NNF. *}
 text {* The type @{text fm} represents simple propositional formulae: *}
 
-datatype_new form = TrueF | FalseF | Less nat nat
+datatype form = TrueF | FalseF | Less nat nat
   | And form form | Or form form | Neg form | ExQ form
 
 primrec interp :: "form \<Rightarrow> ('a::ord) list \<Rightarrow> bool"
@@ -66,7 +66,7 @@
   apply reify
   oops
 
-datatype_new fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
+datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
 
 primrec Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool"
 where
@@ -135,7 +135,7 @@
 text {* Example 2: Simple arithmetic formulae *}
 
 text {* The type @{text num} reflects linear expressions over natural number *}
-datatype_new num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
+datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
 
 text {* This is just technical to make recursive definitions easier. *}
 primrec num_size :: "num \<Rightarrow> nat" 
@@ -252,7 +252,7 @@
 
 text {* Let's lift this to formulae and see what happens *}
 
-datatype_new aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
+datatype aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
   Conj aform aform | Disj aform aform | NEG aform | T | F
 
 primrec linaformsize:: "aform \<Rightarrow> nat"
@@ -331,7 +331,7 @@
   one envornement of different types and show that automatic reification also deals with
   bindings *}
   
-datatype_new rb = BC bool | BAnd rb rb | BOr rb rb
+datatype rb = BC bool | BAnd rb rb | BOr rb rb
 
 primrec Irb :: "rb \<Rightarrow> bool"
 where
@@ -343,7 +343,7 @@
   apply (reify Irb.simps)
 oops
 
-datatype_new rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
+datatype rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
   | INeg rint | ISub rint rint
 
 primrec Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
@@ -370,7 +370,7 @@
   apply (reify Irint_simps ("(3::int) * x + y * y - 9 + (- z)"))
   oops
 
-datatype_new rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
+datatype rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
 
 primrec Irlist :: "rlist \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> int list"
 where
@@ -387,7 +387,7 @@
   apply (reify Irlist.simps Irint_simps ("([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs"))
   oops
 
-datatype_new rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
+datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
   | NNeg rnat | NSub rnat rnat | Nlgth rlist
 
 primrec Irnat :: "rnat \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> nat list \<Rightarrow> nat"
@@ -418,7 +418,7 @@
      ("Suc n * length (([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs)"))
   oops
 
-datatype_new rifm = RT | RF | RVar nat
+datatype rifm = RT | RF | RVar nat
   | RNLT rnat rnat | RNILT rnat rint | RNEQ rnat rnat
   | RAnd rifm rifm | ROr rifm rifm | RImp rifm rifm| RIff rifm rifm
   | RNEX rifm | RIEX rifm | RLEX rifm | RNALL rifm | RIALL rifm | RLALL rifm
@@ -451,7 +451,7 @@
 
 text {* An example for equations containing type variables *}
 
-datatype_new prod = Zero | One | Var nat | Mul prod prod 
+datatype prod = Zero | One | Var nat | Mul prod prod 
   | Pw prod nat | PNM nat nat prod
 
 primrec Iprod :: " prod \<Rightarrow> ('a::linordered_idom) list \<Rightarrow>'a" 
@@ -463,7 +463,7 @@
 | "Iprod (Pw a n) vs = Iprod a vs ^ n"
 | "Iprod (PNM n k t) vs = (vs ! n) ^ k * Iprod t vs"
 
-datatype_new sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
+datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
   | Or sgn sgn | And sgn sgn
 
 primrec Isgn :: "sgn \<Rightarrow> ('a::linordered_idom) list \<Rightarrow> bool"