Sledgehammer: the empty set of fact () should mean nothing, not unchanged
authorblanchet
Fri Apr 16 16:13:49 2010 +0200 (2010-04-16)
changeset 36183f723348b2231
parent 36182 b136019c5d61
child 36184 54a9c0679079
Sledgehammer: the empty set of fact () should mean nothing, not unchanged
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Apr 16 16:08:43 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Apr 16 16:13:49 2010 +0200
     1.3 @@ -27,13 +27,12 @@
     1.4    {add = [], del = ns, only = false}
     1.5  fun only_relevance_override ns : relevance_override =
     1.6    {add = ns, del = [], only = true}
     1.7 -val default_relevance_override = add_to_relevance_override []
     1.8  fun merge_relevance_override_pairwise (r1 : relevance_override)
     1.9                                        (r2 : relevance_override) =
    1.10    {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
    1.11 -   only = #only r1 orelse #only r2}
    1.12 -fun merge_relevance_overrides rs =
    1.13 -  fold merge_relevance_override_pairwise rs default_relevance_override
    1.14 +   only = #only r1 andalso #only r2}
    1.15 +fun merge_relevance_overrides (r, rs) =
    1.16 +  fold merge_relevance_override_pairwise rs r
    1.17  
    1.18  type raw_param = string * string list
    1.19  
    1.20 @@ -274,10 +273,10 @@
    1.21  val parse_relevance_override =
    1.22    Scan.optional (Args.parens
    1.23        (Scan.optional (parse_fact_refs >> only_relevance_override)
    1.24 -                     default_relevance_override
    1.25 +                     (only_relevance_override [])
    1.26         -- Scan.repeat parse_relevance_chunk)
    1.27 -       >> op :: >> merge_relevance_overrides)
    1.28 -      default_relevance_override
    1.29 +       >> merge_relevance_overrides)
    1.30 +      (add_to_relevance_override [])
    1.31  val parse_sledgehammer_command =
    1.32    (Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override
    1.33     -- Scan.option P.nat) #>> sledgehammer_trans
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Apr 16 16:08:43 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Apr 16 16:13:49 2010 +0200
     2.3 @@ -33,7 +33,7 @@
     2.4    let
     2.5      fun aux seen "" = String.implode (rev seen)
     2.6        | aux seen s =
     2.7 -      if String.isPrefix bef s then
     2.8 +        if String.isPrefix bef s then
     2.9            aux seen "" ^ aft ^ aux [] (unprefix bef s)
    2.10          else
    2.11            aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))