changeset 1788 | ca62fab4ce92 |
parent 1668 | 8ead1fe65aad |
child 1845 | afa622bc829d |
--- a/src/HOL/thy_syntax.ML Tue Jun 04 12:49:04 1996 +0200 +++ b/src/HOL/thy_syntax.ML Thu Jun 06 13:13:18 1996 +0200 @@ -84,7 +84,7 @@ val ipairs = "intrs" $$-- repeat1 (ident -- !! string) fun optstring s = optional (s $$-- string) "\"[]\"" >> trim in - repeat1 string -- ipairs -- optstring "monos" -- optstring "con_defs" + repeat1 name -- ipairs -- optstring "monos" -- optstring "con_defs" >> mk_params end;