equal
deleted
inserted
replaced
249 |> Sign.root_path |
249 |> Sign.root_path |
250 |> Sign.add_path (Long_Name.qualifier name) |
250 |> Sign.add_path (Long_Name.qualifier name) |
251 |> f config type_names |
251 |> f config type_names |
252 |> Sign.restore_naming thy)); |
252 |> Sign.restore_naming thy)); |
253 |
253 |
254 val interpretation_data = |
254 val interpretation_data = Named_Target.theory_map o Old_Datatype_Plugin.data_default; |
255 Named_Target.theory_map o Old_Datatype_Plugin.data Plugin_Name.default_filter; |
|
256 |
255 |
257 |
256 |
258 open Old_Datatype_Aux; |
257 open Old_Datatype_Aux; |
259 |
258 |
260 end; |
259 end; |