# HG changeset patch # User wenzelm # Date 1536493700 -7200 # Node ID 22a3790eecaec6ef8edce442150270ca111194aa # Parent b85d509e7cbf9b60e63e6aa3b611ed4fca8082e1 proper binding positions within the defining command transaction; diff -r b85d509e7cbf -r 22a3790eecae src/HOL/Datatype_Examples/Compat.thy --- a/src/HOL/Datatype_Examples/Compat.thy Sun Sep 09 13:44:48 2018 +0200 +++ b/src/HOL/Datatype_Examples/Compat.thy Sun Sep 09 13:48:20 2018 +0200 @@ -177,10 +177,10 @@ [(@{binding N}, [], NoSyn), (@{binding C}, [@{typ 'a}, Type (Sign.full_name @{theory} @{binding l}, [@{typ 'a}])], NoSyn)])]; + +Theory.setup (snd o BNF_LFP_Compat.add_datatype [] l_specs); \ -setup \snd o BNF_LFP_Compat.add_datatype [] l_specs\ - ML \get_descrs @{theory} (1, 1, 1) @{type_name l}\ thm l.exhaust l.map l.induct l.rec l.size @@ -191,10 +191,10 @@ [(@{binding T}, [@{typ 'b}, Type (@{type_name l}, [Type (Sign.full_name @{theory} @{binding t}, [@{typ 'b}])])], NoSyn)])]; + +Theory.setup (snd o BNF_LFP_Compat.add_datatype [] t_specs); \ -setup \snd o BNF_LFP_Compat.add_datatype [] t_specs\ - ML \get_descrs @{theory} (2, 2, 1) @{type_name t}\ thm t.exhaust t.map t.induct t.rec t.size @@ -206,10 +206,10 @@ [(@{binding FT0}, [], NoSyn), (@{binding FT}, [@{typ 'a} --> Type (Sign.full_name @{theory} @{binding ft}, [@{typ 'a}])], NoSyn)])]; + +Theory.setup (snd o BNF_LFP_Compat.add_datatype [] ft_specs); \ -setup \snd o BNF_LFP_Compat.add_datatype [] ft_specs\ - ML \get_descrs @{theory} (1, 1, 1) @{type_name ft}\ thm ft.exhaust ft.induct ft.rec ft.size