equal
deleted
inserted
replaced
196 let |
196 let |
197 val binding = mk_binding config type_name |
197 val binding = mk_binding config type_name |
198 val final_fqn = Sign.full_name thy binding |
198 val final_fqn = Sign.full_name thy binding |
199 val tyargs = |
199 val tyargs = |
200 List.tabulate (arity, rpair @{sort type} o prefix "'" o string_of_int) |
200 List.tabulate (arity, rpair @{sort type} o prefix "'" o string_of_int) |
201 val thy' = |
201 val (_, thy') = |
202 Typedecl.typedecl_global true (mk_binding config type_name, tyargs, NoSyn) thy |
202 Typedecl.typedecl_global {final = true} (mk_binding config type_name, tyargs, NoSyn) thy |
203 |> snd |
|
204 val typ_map_entry = (thf_type, (final_fqn, arity)) |
203 val typ_map_entry = (thf_type, (final_fqn, arity)) |
205 val ty_map' = typ_map_entry :: ty_map |
204 val ty_map' = typ_map_entry :: ty_map |
206 in (ty_map', thy') end |
205 in (ty_map', thy') end |
207 |
206 |
208 |
207 |