--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Sep 09 20:51:36 2014 +0200
@@ -15,7 +15,7 @@
subsection {* Terms *}
-datatype tm = CP poly | Bound nat | Add tm tm | Mul poly tm
+datatype_new tm = CP poly | Bound nat | Add tm tm | Mul poly tm
| Neg tm | Sub tm tm | CNP nat poly tm
(* A size for poly to make inductive proofs simpler*)
@@ -493,7 +493,7 @@
subsection{* Formulae *}
-datatype fm = T| F| Le tm | Lt tm | Eq tm | NEq tm|
+datatype_new fm = T| F| Le tm | Lt tm | Eq tm | NEq tm|
NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm