# HG changeset patch
# User wenzelm
# Date 791210407 -3600
# Node ID e87c01fd0351989798d499c61fae6fb435211c97
# Parent  3a1de9454d1308adff425ade1724aec9563ce4d5
binder: optional body pri now [bracketted];

diff -r 3a1de9454d13 -r e87c01fd0351 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Fri Jan 27 13:35:29 1995 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Fri Jan 27 13:40:07 1995 +0100
@@ -212,12 +212,9 @@
 val infxl = "infixl" $$-- !! nat >> cat "Infixl";
 val infxr = "infixr" $$-- !! nat >> cat "Infixr";
 
-fun mk_binder ((name, x), y) =
-  let val (p1, p2) = if y = "None" then ("0", x) else (x, y);
-  in mk_triple (name, p1, p2) end;
-
-val binder = "binder" $$-- !! (string -- nat -- optional nat "None") 
-             >> (cat "Binder" o mk_binder);
+val binder = "binder" $$--
+  !! (string -- optional ("[" $$-- nat --$$ "]") "0" -- nat)
+  >> (cat "Binder" o mk_triple1);
 
 val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list;