src/HOL/thy_syntax.ML
changeset 12505 46bfc675015a
parent 12180 91c9f661b183
child 14598 7009f59711e3
     1.1 --- a/src/HOL/thy_syntax.ML	Fri Dec 14 11:57:03 2001 +0100
     1.2 +++ b/src/HOL/thy_syntax.ML	Fri Dec 14 22:26:55 2001 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4  val record_decl =
     1.5    (type_args -- name >> (mk_pair o apfst mk_list)) --$$ "="
     1.6      -- optional (typ --$$ "+" >> (parens o cat "Some")) "None"
     1.7 -    -- repeat1 ((name --$$ "::" -- typ) >> mk_pair)
     1.8 +    -- repeat1 ((name --$$ "::" -- !! (typ -- opt_mixfix)) >> mk_triple2)
     1.9    >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]);
    1.10  
    1.11