--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 16 20:50:50 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 16 20:51:15 2010 +0200
@@ -27,12 +27,13 @@
{add = [], del = ns, only = false}
fun only_relevance_override ns : relevance_override =
{add = ns, del = [], only = true}
+val no_relevance_override = add_to_relevance_override []
fun merge_relevance_override_pairwise (r1 : relevance_override)
(r2 : relevance_override) =
{add = #add r1 @ #add r2, del = #del r1 @ #del r2,
only = #only r1 andalso #only r2}
-fun merge_relevance_overrides (r, rs) =
- fold merge_relevance_override_pairwise rs r
+fun merge_relevance_overrides rs =
+ fold merge_relevance_override_pairwise rs (only_relevance_override [])
type raw_param = string * string list
@@ -206,9 +207,6 @@
val refresh_tptpN = "refresh_tptp"
val helpN = "help"
-val addN = "add"
-val delN = "del"
-val onlyN = "only"
fun minimizize_raw_param_name "timeout" = "minimize_timeout"
| minimizize_raw_param_name name = name
@@ -269,14 +267,11 @@
(Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override)
|| (Args.del |-- Args.colon |-- parse_fact_refs
>> del_from_relevance_override)
- || (P.$$$ onlyN |-- Args.colon |-- parse_fact_refs >> only_relevance_override)
+ || (parse_fact_refs >> only_relevance_override)
val parse_relevance_override =
- Scan.optional (Args.parens
- (Scan.optional (parse_fact_refs >> only_relevance_override)
- (only_relevance_override [])
- -- Scan.repeat parse_relevance_chunk)
- >> merge_relevance_overrides)
- (add_to_relevance_override [])
+ Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
+ >> merge_relevance_overrides))
+ (add_to_relevance_override [])
val parse_sledgehammer_command =
(Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override
-- Scan.option P.nat) #>> sledgehammer_trans