src/HOL/Proofs/Extraction/Higman.thy

--- 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