src/HOL/Decision_Procs/Commutative_Ring.thy

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