# HG changeset patch
# User blanchet
# Date 1271427229 -7200
# Node ID f723348b22313758ead3986558aa2c40b0c98597
# Parent  b136019c5d61833c6e72f5d6035a2b1a746f441c
Sledgehammer: the empty set of fact () should mean nothing, not unchanged

diff -r b136019c5d61 -r f723348b2231 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Apr 16 16:08:43 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Apr 16 16:13:49 2010 +0200
@@ -27,13 +27,12 @@
   {add = [], del = ns, only = false}
 fun only_relevance_override ns : relevance_override =
   {add = ns, del = [], only = true}
-val default_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 orelse #only r2}
-fun merge_relevance_overrides rs =
-  fold merge_relevance_override_pairwise rs default_relevance_override
+   only = #only r1 andalso #only r2}
+fun merge_relevance_overrides (r, rs) =
+  fold merge_relevance_override_pairwise rs r
 
 type raw_param = string * string list
 
@@ -274,10 +273,10 @@
 val parse_relevance_override =
   Scan.optional (Args.parens
       (Scan.optional (parse_fact_refs >> only_relevance_override)
-                     default_relevance_override
+                     (only_relevance_override [])
        -- Scan.repeat parse_relevance_chunk)
-       >> op :: >> merge_relevance_overrides)
-      default_relevance_override
+       >> 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
diff -r b136019c5d61 -r f723348b2231 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Apr 16 16:08:43 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Apr 16 16:13:49 2010 +0200
@@ -33,7 +33,7 @@
   let
     fun aux seen "" = String.implode (rev seen)
       | aux seen s =
-      if String.isPrefix bef s then
+        if String.isPrefix bef s then
           aux seen "" ^ aft ^ aux [] (unprefix bef s)
         else
           aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))