src/HOL/Tools/res_atp.ML
changeset 21690 552d20ff9a95
parent 21588 cd0dc678a205
child 21790 9d2761d09d91
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Dec 07 16:46:14 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Dec 07 16:47:36 2006 +0100
     1.3 @@ -462,18 +462,15 @@
     1.4  
     1.5  exception HASH_CLAUSE and HASH_STRING;
     1.6  
     1.7 -(*Catches (for deletion) theorems automatically generated from other theorems*)
     1.8 -fun insert_suffixed_names ht x =
     1.9 -     (Polyhash.insert ht (x^"_iff1", ());
    1.10 -      Polyhash.insert ht (x^"_iff2", ());
    1.11 -      Polyhash.insert ht (x^"_dest", ()));
    1.12 -
    1.13  (*Reject theorems with names like "List.filter.filter_list_def" or
    1.14 -  "Accessible_Part.acc.defs", as these are definitions arising from packages.
    1.15 -  FIXME: this will also block definitions within locales*)
    1.16 +  "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
    1.17  fun is_package_def a =
    1.18 -   length (NameSpace.unpack a) > 2 andalso
    1.19 -   String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a;
    1.20 +  let val names = NameSpace.unpack a
    1.21 +  in
    1.22 +     length names > 2 andalso
    1.23 +     not (hd names = "local") andalso
    1.24 +     String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a
    1.25 +  end;
    1.26  
    1.27  fun make_banned_test xs =
    1.28    let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
    1.29 @@ -481,7 +478,6 @@
    1.30        fun banned s =
    1.31              isSome (Polyhash.peek ht s) orelse is_package_def s
    1.32    in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
    1.33 -      app (insert_suffixed_names ht) (!blacklist @ xs);
    1.34        banned
    1.35    end;
    1.36  
    1.37 @@ -603,12 +599,16 @@
    1.38  (*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
    1.39  fun blacklist_filter ths =
    1.40    if !run_blacklist_filter then
    1.41 -      let val _ = Output.debug("blacklist filter gets " ^ Int.toString (length ths) ^ " theorems")
    1.42 -          val banned = make_banned_test (map #1 ths)
    1.43 +      let val banned = make_banned_test (map #1 ths)
    1.44            fun ok (a,_) = not (banned a)
    1.45 -          val okthms = filter ok ths
    1.46 -          val _ = Output.debug("...and returns " ^ Int.toString (length okthms))
    1.47 -      in  okthms end
    1.48 +          val (good,bad) = List.partition ok ths
    1.49 +      in  if !Output.show_debug_msgs then
    1.50 +             (Output.debug("blacklist filter gets " ^ Int.toString (length ths) ^ " theorems");
    1.51 +              Output.debug("filtered: " ^ space_implode ", " (map #1 bad));
    1.52 +              Output.debug("...and returns " ^ Int.toString (length good)))
    1.53 +          else ();
    1.54 +          good 
    1.55 +      end
    1.56    else ths;
    1.57  
    1.58  (***************************************************************)
    1.59 @@ -855,7 +855,7 @@
    1.60                                         |> ResAxioms.cnf_rules_pairs |> make_unique
    1.61                                         |> restrict_to_logic logic
    1.62                                         |> remove_unwanted_clauses
    1.63 -      val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
    1.64 +      val _ = Output.debug ("included clauses = " ^ Int.toString(length included_cls))
    1.65        val white_cls = ResAxioms.cnf_rules_pairs white_thms
    1.66        (*clauses relevant to goal gl*)
    1.67        val axcls_list = map (fn ngcls => get_relevant_clauses thy included_cls white_cls (map prop_of ngcls)) goal_cls