--- a/src/HOL/Proofs/Extraction/Higman.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Proofs/Extraction/Higman.thy Tue Sep 09 20:51:36 2014 +0200
@@ -14,7 +14,9 @@
based on Coquand and Fridlender \cite{Coquand93}.
*}
-datatype letter = A | B
+datatype_new letter = A | B
+
+datatype_compat letter
inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool"
where
--- a/src/HOL/Proofs/Extraction/Warshall.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Proofs/Extraction/Warshall.thy Tue Sep 09 20:51:36 2014 +0200
@@ -13,7 +13,9 @@
based on Berger, Schwichtenberg and Seisenberger \cite{Berger-JAR-2001}.
*}
-datatype b = T | F
+datatype_new b = T | F
+
+datatype_compat b
primrec
is_path' :: "('a \<Rightarrow> 'a \<Rightarrow> b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"