equal
deleted
inserted
replaced
150 ("type_enc", [name]) |
150 ("type_enc", [name]) |
151 else |
151 else |
152 error ("Unknown parameter: " ^ quote name ^ ".")) |
152 error ("Unknown parameter: " ^ quote name ^ ".")) |
153 |
153 |
154 |
154 |
155 (* Ensure that type systems such as "mono_simple?" and "poly_guards!!" are |
155 (* Ensures that type encodings such as "mono_simple?" and "poly_guards!!" are |
156 handled correctly. *) |
156 read correctly. *) |
157 val implode_param = strip_spaces_except_between_idents o space_implode " " |
157 val implode_param = strip_spaces_except_between_idents o space_implode " " |
158 |
158 |
159 structure Data = Theory_Data |
159 structure Data = Theory_Data |
160 ( |
160 ( |
161 type T = raw_param list |
161 type T = raw_param list |