equal
deleted
inserted
replaced
8 open BNF_LFP_Compat |
8 open BNF_LFP_Compat |
9 |
9 |
10 val compat_plugin = Plugin_Name.declare_setup \<^binding>\<open>compat\<close>; |
10 val compat_plugin = Plugin_Name.declare_setup \<^binding>\<open>compat\<close>; |
11 |
11 |
12 fun compat fp_sugars = |
12 fun compat fp_sugars = |
13 perhaps (try (datatype_compat (map (fst o dest_Type o #T) fp_sugars))); |
13 perhaps (try (datatype_compat (map (dest_Type_name o #T) fp_sugars))); |
14 in |
14 in |
15 Theory.setup (fp_sugars_interpretation compat_plugin compat) |
15 Theory.setup (fp_sugars_interpretation compat_plugin compat) |
16 end |
16 end |
17 \<close> |
17 \<close> |
18 |
18 |