# HG changeset patch
# User blanchet
# Date 1271443875 -7200
# Node ID 35b9f0db49a0b80fed76ca74f9145198f0073354
# Parent  4deef08608ee0fa0d0eb3ca0d3540b0609a0d482
fiddle with Sledgehammer option syntax

diff -r 4deef08608ee -r 35b9f0db49a0 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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