equal
deleted
inserted
replaced
277 (schem_facts @ ths)) |
277 (schem_facts @ ths)) |
278 end |
278 end |
279 |
279 |
280 val metis_lam_transs = [hide_lamsN, lam_liftingN, combinatorsN] |
280 val metis_lam_transs = [hide_lamsN, lam_liftingN, combinatorsN] |
281 |
281 |
|
282 fun set_opt _ x NONE = SOME x |
|
283 | set_opt get x (SOME x0) = |
|
284 error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x) ^ |
|
285 ".") |
282 fun consider_opt s = |
286 fun consider_opt s = |
283 if member (op =) metis_lam_transs s then apsnd (K (SOME s)) |
287 if member (op =) metis_lam_transs s then apsnd (set_opt I s) |
284 else apfst (K (SOME [s])) |
288 else apfst (set_opt hd [s]) |
285 |
289 |
286 val parse_metis_options = |
290 val parse_metis_options = |
287 Scan.optional |
291 Scan.optional |
288 (Args.parens (Parse.short_ident |
292 (Args.parens (Parse.short_ident |
289 -- Scan.option (Parse.$$$ "," |-- Parse.short_ident)) |
293 -- Scan.option (Parse.$$$ "," |-- Parse.short_ident)) |