src/HOL/thy_syntax.ML
changeset 4225 3d9e551bc5a6
parent 4204 7b15e7eee982
child 4226 38c91213f26b
     1.1 --- a/src/HOL/thy_syntax.ML	Thu Nov 13 10:31:42 1997 +0100
     1.2 +++ b/src/HOL/thy_syntax.ML	Thu Nov 13 12:43:17 1997 +0100
     1.3 @@ -36,8 +36,9 @@
     1.4  (** record **)
     1.5  
     1.6  val record_decl =
     1.7 -  name --$$ "=" -- optional (name --$$ "+" >> (parens o cat "Some")) "None" --
     1.8 -  repeat1 ((name --$$ "::" -- typ) >> mk_pair)
     1.9 +  (type_args -- name >> (mk_pair o apfst mk_list)) --$$ "="
    1.10 +    -- optional (typ --$$ "+" >> cat "Some") "None"
    1.11 +    -- repeat1 ((name --$$ "::" -- typ) >> mk_pair)
    1.12    >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]);
    1.13  
    1.14