| changeset 61877 | 276ad4354069 |
| parent 61841 | 4d3527b94f2a |
| child 62519 | a564458f94db |
| 61876:669f47397249 | 61877:276ad4354069 |
|---|---|
161 |
161 |
162 fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2); |
162 fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2); |
163 |
163 |
164 fun string_of_xthm (xref, args) = |
164 fun string_of_xthm (xref, args) = |
165 Facts.string_of_ref xref ^ |
165 Facts.string_of_ref xref ^ |
166 implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src @{context}) args); |
166 implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src @{context}) args); |
167 |
167 |
168 val parse_fact_refs = |
168 val parse_fact_refs = |
169 Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.xthm >> string_of_xthm)); |
169 Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.xthm >> string_of_xthm)); |
170 |
170 |
171 val parse_attr = |
171 val parse_attr = |