src/Pure/Thy/thy_parse.ML
changeset 1027 651637377289
parent 889 e87c01fd0351
child 1235 b4056a71eca2
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Apr 10 08:49:00 1995 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue Apr 11 11:20:43 1995 +0200
     1.3 @@ -213,8 +213,10 @@
     1.4  val infxr = "infixr" $$-- !! nat >> cat "Infixr";
     1.5  
     1.6  val binder = "binder" $$--
     1.7 -  !! (string -- optional ("[" $$-- nat --$$ "]") "0" -- nat)
     1.8 -  >> (cat "Binder" o mk_triple1);
     1.9 +  !! (string -- ( ("[" $$-- nat --$$ "]") -- nat
    1.10 +                || nat >> (fn n => (n,n))
    1.11 +     )          )
    1.12 +  >> (cat "Binder" o mk_triple2);
    1.13  
    1.14  val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list;
    1.15