137 |
137 |
138 (** Pure syntax **) |
138 (** Pure syntax **) |
139 |
139 |
140 val pure_types = |
140 val pure_types = |
141 map (fn t => (t, 0, NoSyn)) |
141 map (fn t => (t, 0, NoSyn)) |
142 (terminals @ [logic, "type", "types", "sort", "classes", args, |
142 (terminals @ [logic, "type", "types", "sort", "classes", args, cargs, |
143 "pttrn", "idt", "idts", "aprop", "asms", any, sprop]); |
143 "pttrn", "idt", "idts", "aprop", "asms", any, sprop]); |
144 |
144 |
145 val pure_syntax = |
145 val pure_syntax = |
146 [("_lambda", "[idts, 'a] => logic", Mixfix ("(3%_./ _)", [], 0)), |
146 [("_lambda", "[idts, 'a] => logic", Mixfix ("(3%_./ _)", [], 0)), |
147 ("_abs", "'a", NoSyn), |
147 ("_abs", "'a", NoSyn), |