binder: optional body pri now [bracketted];
authorwenzelm
Fri Jan 27 13:40:07 1995 +0100 (1995-01-27)
changeset 889e87c01fd0351
parent 888 3a1de9454d13
child 890 2b7275b13bef
binder: optional body pri now [bracketted];
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Jan 27 13:35:29 1995 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Fri Jan 27 13:40:07 1995 +0100
     1.3 @@ -212,12 +212,9 @@
     1.4  val infxl = "infixl" $$-- !! nat >> cat "Infixl";
     1.5  val infxr = "infixr" $$-- !! nat >> cat "Infixr";
     1.6  
     1.7 -fun mk_binder ((name, x), y) =
     1.8 -  let val (p1, p2) = if y = "None" then ("0", x) else (x, y);
     1.9 -  in mk_triple (name, p1, p2) end;
    1.10 -
    1.11 -val binder = "binder" $$-- !! (string -- nat -- optional nat "None") 
    1.12 -             >> (cat "Binder" o mk_binder);
    1.13 +val binder = "binder" $$--
    1.14 +  !! (string -- optional ("[" $$-- nat --$$ "]") "0" -- nat)
    1.15 +  >> (cat "Binder" o mk_triple1);
    1.16  
    1.17  val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list;
    1.18