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 true --| Scan.lift (@{keyword "="})) -- Args.const_proper true >> |
74 ((Args.type_name true --| Scan.lift @{keyword "="}) -- Args.const_proper true >> |
75 (fn (tyname, relname) => |
75 (fn (tyname, relname) => |
76 let val minfo = {relmap = relname} |
76 let val minfo = {relmap = relname} |
77 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)) |
78 "declaration of map information" |
78 "declaration of map information" |
79 |
79 |