# HG changeset patch
# User wenzelm
# Date 936629761 -7200
# Node ID 31a25b6af1b3c0ebacf758e6a2a3276f63608a87
# Parent  9deae880cf740b5715dd956f5018cc17f1133a54
removed thms_closure (unused);

diff -r 9deae880cf74 -r 31a25b6af1b3 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Sep 06 12:49:39 1999 +0200
+++ b/src/Pure/pure_thy.ML	Mon Sep 06 16:56:01 1999 +0200
@@ -25,7 +25,6 @@
 sig
   include BASIC_PURE_THY
   val cond_extern_thm_sg: Sign.sg -> string -> xstring
-  val thms_closure: theory -> xstring -> thm list option
   val thms_containing: theory -> string list -> (string * thm) list
   val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm
   val smart_store_thms: (bstring * thm list) -> thm list
@@ -108,23 +107,11 @@
 
 (** retrieve theorems **)
 
-(* thms_closure *)
-
-(*note: we avoid life references to the theory, so users may safely
-  keep thms_closure with moderate space consumption*)
-
-fun thms_closure_aux thy =
-  let val ref {space, thms_tab, ...} = get_theorems thy
-  in fn name => Symtab.lookup (thms_tab, NameSpace.intern space name) end;
-
-fun thms_closure thy =
-  let val closures = map thms_closure_aux (thy :: Theory.ancestors_of thy)
-  in fn name => get_first (fn f => f name) closures end;
-
-
 (* get_thms etc. *)
 
-fun lookup_thms name thy = thms_closure_aux thy name;
+fun lookup_thms name thy =
+  let val ref {space, thms_tab, ...} = get_theorems thy
+  in Symtab.lookup (thms_tab, NameSpace.intern space name) end;
 
 fun get_thms thy name =
   (case get_first (lookup_thms name) (thy :: Theory.ancestors_of thy) of