equal
deleted
inserted
replaced
280 let val parse_flag = |
280 let val parse_flag = |
281 Args.$$$ "no_quantify" >> K (apfst (K false)) |
281 Args.$$$ "no_quantify" >> K (apfst (K false)) |
282 || Args.$$$ "abs" >> K (apsnd (K true)); |
282 || Args.$$$ "abs" >> K (apsnd (K true)); |
283 in |
283 in |
284 Method.simple_args |
284 Method.simple_args |
285 (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >> |
285 (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >> |
286 curry (foldl op |>) (true, false)) |
286 curry (foldl op |>) (true, false)) |
287 (fn (q,a) => fn _ => meth q a 1) |
287 (fn (q,a) => fn _ => meth q a 1) |
288 end; |
288 end; |
289 |
289 |
290 fun presburger_method q a i = Method.METHOD (fn facts => |
290 fun presburger_method q a i = Method.METHOD (fn facts => |