major tuning;

--- a/src/Pure/fact_index.ML	Sun May 22 16:51:07 2005 +0200
+++ b/src/Pure/fact_index.ML	Sun May 22 16:51:08 2005 +0200
@@ -2,24 +2,27 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Facts indexed by consts or (some) frees.
+Facts indexed by consts or frees.
 *)
 
 signature FACT_INDEX =
 sig
-  val index_term: (string -> bool) -> (string list * string list) * term
-    -> string list * string list
-  val index_thm: (string -> bool) -> (string list * string list) * thm
-    -> string list * string list
+  type spec
+  val index_term: (string -> bool) -> term -> spec -> spec
+  val index_thm: (string -> bool) -> thm -> spec -> spec
   type T
+  val facts: T -> (string * thm list) list
   val empty: T
-  val add: (string -> bool) -> T * (string * thm list) -> T
-  val find: string list * string list -> T -> (string * thm list) list
+  val add: (string -> bool) -> (string * thm list) -> T -> T
+  val find: T -> spec -> (string * thm list) list
 end;
 
 structure FactIndex: FACT_INDEX =
 struct
 
+type spec = string list * string list;
+
+
 (* indexing items *)
 
 fun add_frees pred (Free (x, _), xs) = if pred x then x ins_string xs else xs
@@ -27,12 +30,16 @@
   | add_frees pred (Abs (_, _, t), xs) = add_frees pred (t, xs)
   | add_frees _ (_, xs) = xs;
 
-fun index_term pred ((cs, xs), t) =
+fun index_term pred t (cs, xs) =
   (Term.add_term_consts (t, cs) \ Term.dummy_patternN, add_frees pred (t, xs));
 
-fun index_thm pred (idx, th) =
-  let val {hyps, prop, ...} = Thm.rep_thm th
-  in Library.foldl (index_term pred) (index_term pred (idx, prop), hyps) end;
+fun index_thm pred th idx =
+  let val {tpairs, hyps, prop, ...} = Thm.rep_thm th in
+    idx
+    |> index_term pred prop
+    |> fold (index_term pred) hyps
+    |> fold (index_term pred) (Thm.terms_of_tpairs tpairs)
+  end;
 
 
 (* build index *)
@@ -41,16 +48,18 @@
   consts: (int * (string * thm list)) list Symtab.table,
   frees: (int * (string * thm list)) list Symtab.table};
 
+fun facts (Index {facts, ...}) = facts;
+
 val empty =
   Index {next = 0, facts = [], consts = Symtab.empty, frees = Symtab.empty};
 
-fun add pred (Index {next, facts, consts, frees}, (name, ths)) =
+fun add pred (name, ths) (Index {next, facts, consts, frees}) =
   let
-    fun upd (tab, a) = Symtab.update_multi ((a, (next, (name, ths))), tab);
-    val (cs, xs) = Library.foldl (index_thm pred) (([], []), ths);
+    fun upd a tab = Symtab.update_multi ((a, (next, (name, ths))), tab);
+    val (cs, xs) = fold (index_thm pred) ths ([], []);
   in
     Index {next = next + 1, facts = (name, ths) :: facts,
-      consts = Library.foldl upd (consts, cs), frees = Library.foldl upd (frees, xs)}
+      consts = fold upd cs consts, frees = fold upd xs frees}
   end;
 
 
@@ -64,10 +73,10 @@
       else intersect (xxs, ys);
 
 fun intersects [xs] = xs
-  | intersects xss = if exists null xss then [] else Library.foldl intersect (hd xss, tl xss);
+  | intersects xss = if exists null xss then [] else foldr1 intersect xss;
 
-fun find ([], []) (Index {facts, ...}) = facts
-  | find (cs, xs) (Index {consts, frees, ...}) =
+fun find idx ([], []) = facts idx
+  | find (Index {consts, frees, ...}) (cs, xs) =
       (map (curry Symtab.lookup_multi consts) cs @
         map (curry Symtab.lookup_multi frees) xs) |> intersects |> map #2;