# HG changeset patch
# User wenzelm
# Date 1205600881 -3600
# Node ID 1e007f3f426ea2d71ec7162b3aac2721bd6bad52
# Parent  e8440c90c4749ce8fbec90fb941b39ccffdcf92f
obsolete (cf. facts.ML);

diff -r e8440c90c474 -r 1e007f3f426e src/Pure/fact_index.ML
--- a/src/Pure/fact_index.ML	Sat Mar 15 18:08:00 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,101 +0,0 @@
-(*  Title:      Pure/fact_index.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Facts indexed by consts or frees.
-*)
-
-signature FACT_INDEX =
-sig
-  type spec
-  type T
-  val facts: T -> (string * thm list) list
-  val props: T -> thm list
-  val could_unify: T -> term -> thm list
-  val empty: T
-  val add_local: bool -> bool -> (string * thm list) -> T -> T
-  val add_global: (string * thm list) -> T -> T
-  val find: T -> spec -> (string * thm list) list
-end;
-
-structure FactIndex: FACT_INDEX =
-struct
-
-
-(* indexing items *)
-
-type spec = string list * string list;
-
-val add_consts = fold_aterms
-  (fn Const (c, _) => if c = Term.dummy_patternN then I else insert (op =) c | _ => I);
-
-val add_frees = fold_aterms (fn Free (x, _) => insert (op =) x | _ => I);
-
-fun index_term t (cs, xs) = (add_consts t cs, add_frees t xs);
-
-fun index_thm th =
-  let val {tpairs, hyps, prop, ...} = Thm.rep_thm th in
-    index_term prop
-    #> fold index_term hyps
-    #> fold (fn (t, u) => index_term t #> index_term u) tpairs
-  end;
-
-
-(* build index *)
-
-type fact = string * thm list;
-
-datatype T = Index of
- {facts: fact list,
-  consts: (serial * fact) list Symtab.table,
-  frees: (serial * fact) list Symtab.table,
-  props: thm Net.net};
-
-fun facts (Index {facts, ...}) = facts;
-fun props (Index {props, ...}) =
-  sort_distinct (Term.term_ord o pairself Thm.full_prop_of) (Net.content props);
-fun could_unify (Index {props, ...}) = Net.unify_term props;
-
-val empty =
-  Index {facts = [], consts = Symtab.empty, frees = Symtab.empty, props = Net.empty};
-
-fun add_local do_props do_index (fact as (_, ths)) (Index {facts, consts, frees, props}) =
-  let
-    val entry = (serial (), fact);
-    val (cs, xs) = fold index_thm ths ([], []);
-
-    val (facts', consts', frees') =
-      if do_index then
-       (fact :: facts,
-        consts |> fold (fn c => Symtab.cons_list (c, entry)) cs,
-        frees |> fold (fn x => Symtab.cons_list (x, entry)) xs)
-      else (facts, consts, frees);
-    val props' =
-      if do_props then props |> fold (fn th => Net.insert_term (K false) (Thm.prop_of th, th)) ths
-      else props;
-  in Index {facts = facts', consts = consts', frees = frees', props = props'} end;
-
-val add_global = add_local false true;
-
-
-(* find by consts/frees *)
-
-local
-
-fun fact_ord ((i, _), (j, _)) = int_ord (j, i);
-
-fun intersects [xs] = xs
-  | intersects xss =
-      if exists null xss then []
-      else fold (OrdList.inter fact_ord) (tl xss) (hd xss);
-
-in
-
-fun find idx ([], []) = facts idx
-  | find (Index {consts, frees, ...}) (cs, xs) =
-      (map (Symtab.lookup_list consts) cs @
-        map (Symtab.lookup_list frees) xs) |> intersects |> map #2;
-
-end
-
-end;