# HG changeset patch
# User paulson
# Date 865509372 -7200
# Node ID 0c4efa9eac29ec46704c84a4bc167073c4856fc9
# Parent  dfd9cbad5530f29b6f87eef9d7a0726f4f19f5dd
A slight simplification of optstring

diff -r dfd9cbad5530 -r 0c4efa9eac29 src/ZF/thy_syntax.ML
--- 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