equal
deleted
inserted
replaced
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 **) |
|
43 |
|
44 (*Skipping initial blanks, find the first identifier*) (* FIXME slightly broken! *) |
|
45 fun scan_to_id s = |
|
46 s |> Symbol.explode |
|
47 |> Scan.error (Scan.finite Symbol.stopper |
|
48 (Scan.!! (fn _ => "Expected to find an identifier in " ^ s) |
|
49 (Scan.any Symbol.is_blank |-- Syntax.scan_id))) |
|
50 |> #1; |
43 |
51 |
44 fun inductive_decl coind = |
52 fun inductive_decl coind = |
45 let |
53 let |
46 val no_atts = map (mk_pair o rpair "[]"); |
54 val no_atts = map (mk_pair o rpair "[]"); |
47 fun mk_intr_name (s, _) = (*the "op" cancels any infix status*) |
55 fun mk_intr_name (s, _) = (*the "op" cancels any infix status*) |