--- a/src/ZF/thy_syntax.ML Thu Jun 05 13:15:36 1997 +0200
+++ b/src/ZF/thy_syntax.ML Thu Jun 05 13:16:12 1997 +0200
@@ -60,7 +60,7 @@
end
val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string
val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
- fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
+ fun optstring s = optional (s $$-- string >> trim) "[]"
in domains -- ipairs -- optstring "monos" -- optstring "con_defs"
-- optstring "type_intrs" -- optstring "type_elims"
>> mk_params