equal
deleted
inserted
replaced
5 ML \<open> |
5 ML \<open> |
6 let |
6 let |
7 open BNF_FP_Def_Sugar |
7 open BNF_FP_Def_Sugar |
8 open BNF_LFP_Compat |
8 open BNF_LFP_Compat |
9 |
9 |
10 val compat_plugin = Plugin_Name.declare_setup @{binding compat}; |
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 (fst o dest_Type 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) |