equal
deleted
inserted
replaced
69 |
69 |
70 (* FIXME export proper internal update operation!? *) |
70 (* FIXME export proper internal update operation!? *) |
71 |
71 |
72 val quotmaps_attribute_setup = |
72 val quotmaps_attribute_setup = |
73 Attrib.setup @{binding map} |
73 Attrib.setup @{binding map} |
74 ((Args.type_name false --| Scan.lift (@{keyword "="})) -- (* FIXME Args.type_name true (requires "set" type) *) |
74 ((Args.type_name true --| Scan.lift (@{keyword "="})) -- Args.const_proper true >> |
75 Args.const_proper true >> |
|
76 (fn (tyname, relname) => |
75 (fn (tyname, relname) => |
77 let val minfo = {relmap = relname} |
76 let val minfo = {relmap = relname} |
78 in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end)) |
77 in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end)) |
79 "declaration of map information" |
78 "declaration of map information" |
80 |
79 |