equal
deleted
inserted
replaced
108 val tyname = Sign.intern_type thy tystr |
108 val tyname = Sign.intern_type thy tystr |
109 val mapname = Sign.intern_const thy mapstr |
109 val mapname = Sign.intern_const thy mapstr |
110 val relname = Sign.intern_const thy relstr |
110 val relname = Sign.intern_const thy relstr |
111 |
111 |
112 fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ()) |
112 fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ()) |
113 val _ = List.app sanity_check [mapname, relname] |
113 val _ = List.app sanity_check [mapname, relname] |
114 in |
114 in |
115 maps_attribute_aux tyname {mapfun = mapname, relmap = relname} |
115 maps_attribute_aux tyname {mapfun = mapname, relmap = relname} |
116 end |
116 end |
117 |
117 |
118 val maps_attr_parser = |
118 val maps_attr_parser = |