equal
deleted
inserted
replaced
32 (** record **) |
32 (** record **) |
33 |
33 |
34 val record_decl = |
34 val record_decl = |
35 (type_args -- name >> (mk_pair o apfst mk_list)) --$$ "=" |
35 (type_args -- name >> (mk_pair o apfst mk_list)) --$$ "=" |
36 -- optional (typ --$$ "+" >> (parens o cat "Some")) "None" |
36 -- optional (typ --$$ "+" >> (parens o cat "Some")) "None" |
37 -- repeat1 ((name --$$ "::" -- typ) >> mk_pair) |
37 -- repeat1 ((name --$$ "::" -- !! (typ -- opt_mixfix)) >> mk_triple2) |
38 >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]); |
38 >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]); |
39 |
39 |
40 |
40 |
41 |
41 |
42 (** (co)inductive **) |
42 (** (co)inductive **) |