# HG changeset patch
# User wenzelm
# Date 965847622 -7200
# Node ID 391f3ee75b1e39328953fde58810af6e7a85ccf1
# Parent  216d053992a568623d98660fafd1efef43ca9625
added get_thms_closure, single_thm;

diff -r 216d053992a5 -r 391f3ee75b1e src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Aug 09 20:59:23 2000 +0200
+++ b/src/Pure/pure_thy.ML	Wed Aug 09 21:00:22 2000 +0200
@@ -25,6 +25,8 @@
 signature PURE_THY =
 sig
   include BASIC_PURE_THY
+  val get_thms_closure: theory -> xstring -> thm list
+  val single_thm: string -> thm list -> thm
   val cond_extern_thm_sg: Sign.sg -> string -> xstring
   val thms_containing: theory -> string list -> (string * thm) list
   val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm
@@ -115,23 +117,42 @@
 
 (** retrieve theorems **)
 
-(* get_thms etc. *)
+(* selections *)
+
+fun the_thms _ (Some thms) = thms
+  | the_thms name None = error ("Unknown theorem(s) " ^ quote 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 single_thm _ [thm] = thm
+  | single_thm name _ = error ("Single theorem expected " ^ quote name);
+
+
+(* get_thms_closure -- statically scoped *)
+
+(*beware of proper order of evaluation!*)
 
-fun get_thms thy name =
-  (case get_first (lookup_thms name) (thy :: Theory.ancestors_of thy) of
-    None => raise THEORY ("Unknown theorem(s) " ^ quote name, [thy])
-  | Some thms => map (Thm.transfer thy) thms);
+fun lookup_thms thy =
+  let
+    val sg_ref = Sign.self_ref (Theory.sign_of thy);
+    val ref {space, thms_tab, ...} = get_theorems thy;
+  in
+    fn name =>
+      apsome (map (Thm.transfer_sg (Sign.deref sg_ref)))  	(*semi-dynamic identity*)
+      (Symtab.lookup (thms_tab, NameSpace.intern space name))   (*static content*)
+  end;
 
-fun get_thm thy name =
-  (case get_thms thy name of
-    [thm] => thm
-  | _ => raise THEORY ("Single theorem expected " ^ quote name, [thy]));
+fun get_thms_closure thy =
+  let val closures = map lookup_thms (thy :: Theory.ancestors_of thy)
+  in fn name => the_thms name (get_first (fn f => f name) closures) end;
+
+
+(* get_thm etc. *)
+
+fun get_thms theory name =
+  get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory)
+  |> the_thms name |> map (Thm.transfer theory);
 
 fun get_thmss thy names = flat (map (get_thms thy) names);
+fun get_thm thy name = single_thm name (get_thms thy name);
 
 
 (* thms_of *)