add_local: simplified interface, all frees are known'';
authorwenzelm
Wed Jul 19 12:11:59 2006 +0200 (2006-07-19)
changeset 201567a7898b1cfa4
parent 20155 da0505518e69
child 20157 28638d2a6bc7
add_local: simplified interface, all frees are known'';
src/Pure/fact_index.ML
     1.1 --- a/src/Pure/fact_index.ML	Wed Jul 19 12:11:57 2006 +0200
     1.2 +++ b/src/Pure/fact_index.ML	Wed Jul 19 12:11:59 2006 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4    val could_unify: T -> term -> thm list
     1.5    val empty: T
     1.6    val add_global: (string * thm list) -> T -> T
     1.7 -  val add_local: bool -> (string -> bool) -> (string * thm list) -> T -> T
     1.8 +  val add_local: bool -> (string * thm list) -> T -> T
     1.9    val find: T -> spec -> (string * thm list) list
    1.10  end;
    1.11  
    1.12 @@ -29,17 +29,15 @@
    1.13  val add_consts = fold_aterms
    1.14    (fn Const (c, _) => if c = Term.dummy_patternN then I else insert (op =) c | _ => I);
    1.15  
    1.16 -fun add_frees known = fold_aterms
    1.17 -  (fn Free (x, _) => if known x then insert (op =) x else I | _ => I);
    1.18 +val add_frees = fold_aterms (fn Free (x, _) => insert (op =) x | _ => I);
    1.19  
    1.20 -fun index_term known t (cs, xs) = (add_consts t cs, add_frees known t xs);
    1.21 +fun index_term t (cs, xs) = (add_consts t cs, add_frees t xs);
    1.22  
    1.23 -fun index_thm known th idx =
    1.24 +fun index_thm th =
    1.25    let val {tpairs, hyps, prop, ...} = Thm.rep_thm th in
    1.26 -    idx
    1.27 -    |> index_term known prop
    1.28 -    |> fold (index_term known) hyps
    1.29 -    |> fold (fn (t, u) => index_term known t #> index_term known u) tpairs
    1.30 +    index_term prop
    1.31 +    #> fold index_term hyps
    1.32 +    #> fold (fn (t, u) => index_term t #> index_term u) tpairs
    1.33    end;
    1.34  
    1.35  
    1.36 @@ -61,10 +59,10 @@
    1.37  val empty =
    1.38    Index {facts = [], consts = Symtab.empty, frees = Symtab.empty, props = Net.empty};
    1.39  
    1.40 -fun add do_props do_index known (fact as (_, ths)) (Index {facts, consts, frees, props}) =
    1.41 +fun add do_props do_index (fact as (_, ths)) (Index {facts, consts, frees, props}) =
    1.42    let
    1.43      val entry = (serial (), fact);
    1.44 -    val (cs, xs) = fold (index_thm known) ths ([], []);
    1.45 +    val (cs, xs) = fold index_thm ths ([], []);
    1.46  
    1.47      val (facts', consts', frees') =
    1.48        if do_index then
    1.49 @@ -77,7 +75,7 @@
    1.50        else props;
    1.51    in Index {facts = facts', consts = consts', frees = frees', props = props'} end;
    1.52  
    1.53 -val add_global = add false true (K false);
    1.54 +val add_global = add false true;
    1.55  val add_local = add true;
    1.56  
    1.57