# HG changeset patch
# User blanchet
# Date 1409695582 -7200
# Node ID 2bf3ed0f62cf08e4a3445ede73b5a64b2b1319e2
# Parent  72fc2bf5298615bebcb69ebfab1e1fe71c1b6765
giving up calling 'datatype_compat' in a locale -- causes trouble with extensions

diff -r 72fc2bf52986 -r 2bf3ed0f62cf src/HOL/BNF_Examples/Compat.thy
--- 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>