src/HOL/Decision_Procs/Commutative_Ring.thy

--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -11,12 +11,12 @@
 
 text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *}
 
-datatype_new 'a pol =
+datatype 'a pol =
     Pc 'a
   | Pinj nat "'a pol"
   | PX "'a pol" nat "'a pol"
 
-datatype_new 'a polex =
+datatype 'a polex =
     Pol "'a pol"
   | Add "'a polex" "'a polex"
   | Sub "'a polex" "'a polex"