# HG changeset patch
# User wenzelm
# Date 1025617069 -7200
# Node ID eb0b565909a0021306dd1103bdfffb824623cc3a
# Parent  d0859ff6cd651c4e3087cfdbcc8401f6fc7e7b1b
emulate old thms_containing;

diff -r d0859ff6cd65 -r eb0b565909a0 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Tue Jul 02 15:36:51 2002 +0200
+++ b/src/Pure/goals.ML	Tue Jul 02 15:37:49 2002 +0200
@@ -118,7 +118,7 @@
   val setup: (theory -> theory) list
 end;
 
-structure Goals : GOALS =
+structure Goals: GOALS =
 struct
 
 (*** Old-style locales ***)
@@ -1130,38 +1130,24 @@
   let
     val thy = theory_of_goal ();
     val consts = map (Sign.intern_const (Theory.sign_of thy)) raw_consts;
-  in ThmDatabase.thms_containing thy consts end;
-
+  in
+    (case filter (is_none o Sign.const_type (Theory.sign_of thy)) consts of
+      [] => ()
+    | cs => error ("thms_containing: undeclared consts " ^ commas_quote cs));
+    PureThy.thms_containing thy (consts, [])
+    |> map #2 |> flat
+    |> map (fn th => (Thm.name_of_thm th, th))
+  end;
 
 (*top_const: main constant, ignoring Trueprop*)
 fun top_const (_ $ t) = (case head_of t of Const (c, _) => Some c | _ => None)
   | top_const _ = None;
 
 val intro_const = top_const o concl_of;
-
 fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const p;
 
-(* In case faster access is necessary, the thm db should provide special
-functions
-
-index_intros, index_elims: string -> (string * thm) list
-
-where thm [| A1 ; ...; An |] ==> B is returned by
-- index_intros c if B  is of the form c t1 ... tn
-- index_elims c  if A1 is of the form c t1 ... tn
-*)
-
-(* could be provided by thm db *)
-fun index_intros c =
-  let fun topc(_,thm) = intro_const thm = Some(c);
-      val named_thms = ThmDatabase.thms_containing (theory_of_goal ()) [c]
-  in filter topc named_thms end;
-
-(* could be provided by thm db *)
-fun index_elims c =
-  let fun topc(_,thm) = elim_const thm = Some(c);
-      val named_thms = ThmDatabase.thms_containing (theory_of_goal ()) [c]
-  in filter topc named_thms end;
+fun index_intros c = thms_containing [c] |> filter (fn (_, thm) => intro_const thm = Some c);
+fun index_elims c = thms_containing [c] |> filter (fn (_, thm) => elim_const thm = Some c);
 
 (*assume that parameters have unique names; reverse them for substitution*)
 fun goal_params i =