equal
deleted
inserted
replaced
234 |> Data.map (fold2 (fn T_name => fn gen_size_name => |
234 |> Data.map (fold2 (fn T_name => fn gen_size_name => |
235 Symtab.update_new (T_name, (gen_size_name, (gen_size_simps, flat gen_size_map_thmss)))) |
235 Symtab.update_new (T_name, (gen_size_name, (gen_size_simps, flat gen_size_map_thmss)))) |
236 T_names gen_size_names) |
236 T_names gen_size_names) |
237 end; |
237 end; |
238 |
238 |
239 val _ = Theory.setup (fp_sugar_interpretation generate_size); |
239 (* FIXME: get rid of "perhaps o try" once the code is stable *) |
|
240 val _ = Theory.setup (fp_sugar_interpretation (perhaps o try o generate_size)); |
240 |
241 |
241 end; |
242 end; |