proper header;
authorwenzelm
Thu Oct 29 16:07:27 2009 +0100 (2009-10-29)
changeset 333095f67433e6dd8
parent 33308 cf62d1690d04
child 33310 44f9665c2091
proper header;
adapted ResBlacklist -- eliminated inefficient hash table;
eliminated some old folds;
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Oct 29 16:06:15 2009 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Oct 29 16:07:27 2009 +0100
     1.3 @@ -1,4 +1,6 @@
     1.4 -(*  Author:     Jia Meng, Cambridge University Computer Laboratory, NICTA *)
     1.5 +(*  Title:      HOL/Tools/res_atp.ML
     1.6 +    Author:     Jia Meng, Cambridge University Computer Laboratory, NICTA
     1.7 +*)
     1.8  
     1.9  signature RES_ATP =
    1.10  sig
    1.11 @@ -366,29 +368,29 @@
    1.12      val local_facts = ProofContext.facts_of ctxt;
    1.13    in valid_facts global_facts @ valid_facts local_facts end;
    1.14  
    1.15 -fun multi_name a (th, (n,pairs)) =
    1.16 -  (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
    1.17 +fun multi_name a th (n, pairs) =
    1.18 +  (n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs);
    1.19  
    1.20 -fun add_single_names ((a, []), pairs) = pairs
    1.21 -  | add_single_names ((a, [th]), pairs) = (a,th)::pairs
    1.22 -  | add_single_names ((a, ths), pairs) = #2 (List.foldl (multi_name a) (1,pairs) ths);
    1.23 +fun add_single_names (a, []) pairs = pairs
    1.24 +  | add_single_names (a, [th]) pairs = (a, th) :: pairs
    1.25 +  | add_single_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs));
    1.26  
    1.27  (*Ignore blacklisted basenames*)
    1.28 -fun add_multi_names ((a, ths), pairs) =
    1.29 -  if (Long_Name.base_name a) mem_string ResAxioms.multi_base_blacklist  then pairs
    1.30 -  else add_single_names ((a, ths), pairs);
    1.31 +fun add_multi_names (a, ths) pairs =
    1.32 +  if (Long_Name.base_name a) mem_string ResAxioms.multi_base_blacklist then pairs
    1.33 +  else add_single_names (a, ths) pairs;
    1.34  
    1.35  fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
    1.36  
    1.37  (*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*)
    1.38  fun name_thm_pairs ctxt =
    1.39 -  let val (mults, singles) = List.partition is_multi (all_valid_thms ctxt)
    1.40 -      val ht = mk_clause_table 900   (*ht for blacklisted theorems*)
    1.41 -      fun blacklisted x = run_blacklist_filter andalso is_some (Polyhash.peek ht x)
    1.42 +  let
    1.43 +    val (mults, singles) = List.partition is_multi (all_valid_thms ctxt)
    1.44 +    fun blacklisted (_, th) =
    1.45 +      run_blacklist_filter andalso ResBlacklist.blacklisted ctxt th
    1.46    in
    1.47 -      app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt);
    1.48 -      filter (not o blacklisted o #2)
    1.49 -        (List.foldl add_single_names (List.foldl add_multi_names [] mults) singles)
    1.50 +    filter_out blacklisted
    1.51 +      (fold add_single_names singles (fold add_multi_names mults []))
    1.52    end;
    1.53  
    1.54  fun check_named ("", th) =