equal
deleted
inserted
replaced
161 Datatype_Data.register infos |
161 Datatype_Data.register infos |
162 #> Datatype_Data.interpretation_data (Datatype_Aux.default_config, map fst infos) |
162 #> Datatype_Data.interpretation_data (Datatype_Aux.default_config, map fst infos) |
163 in |
163 in |
164 lthy |
164 lthy |
165 |> Local_Theory.raw_theory register_interpret |
165 |> Local_Theory.raw_theory register_interpret |
166 |> Local_Theory.notes all_notes |> snd |
166 |> Local_Theory.notes all_notes |
|
167 |> snd |
167 end; |
168 end; |
168 |
169 |
169 val _ = |
170 val _ = |
170 Outer_Syntax.local_theory @{command_spec "datatype_compat"} |
171 Outer_Syntax.local_theory @{command_spec "datatype_compat"} |
171 "register new-style datatypes as old-style datatypes" |
172 "register new-style datatypes as old-style datatypes" |