giving up calling 'datatype_compat' in a locale -- causes trouble with extensions

--- a/src/HOL/BNF_Examples/Compat.thy	Wed Sep 03 00:06:22 2014 +0200
+++ b/src/HOL/BNF_Examples/Compat.thy	Wed Sep 03 00:06:22 2014 +0200
@@ -165,18 +165,6 @@
 | "f_foo (FooCons bar foo) = Suc (f_foo foo) + f_bar bar"
 | "f_bar Bar = Suc 0"
 
-locale opt begin
-
-datatype_new 'a opt = Non | Som 'a
-
-ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name opt}; \<close>
-
-datatype_compat opt
-
-ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name opt}; \<close>
-
-end
-
 datatype funky = Funky "funky tre" | Funky'
 
 ML \<open> get_descrs @{theory} (3, 3, 3) @{type_name funky}; \<close>