# HG changeset patch
# User wenzelm
# Date 1164670523 -3600
# Node ID c097a926ba78641809dafb61e63b6434abf0fbc3
# Parent  af2932baf0685c930888f5a01e704793368a9bf7
added burrow_fact;
no export of name_thms(s);

diff -r af2932baf068 -r c097a926ba78 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Nov 28 00:35:21 2006 +0100
+++ b/src/Pure/pure_thy.ML	Tue Nov 28 00:35:23 2006 +0100
@@ -57,8 +57,7 @@
   val thms_of: theory -> (string * thm) list
   val all_thms_of: theory -> (string * thm) list
   val hide_thms: bool -> string list -> theory -> theory
-  val name_thms: bool -> string -> thm list -> thm list
-  val name_thmss: string -> (thm list * 'a) list -> (thm list * 'a) list
+  val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
   val store_thm: (bstring * thm) * attribute list -> theory -> thm * theory
   val smart_store_thms: (bstring * thm list) -> thm list
   val smart_store_thms_open: (bstring * thm list) -> thm list
@@ -322,11 +321,8 @@
 
 fun name_thms pre name xs = map (name_thm pre) (name_multi name xs);
 
-fun name_thmss name xs =
-  (case filter_out (null o fst) xs of
-    [([x], z)] => [([name_thm true (name, x)], z)]
-  | _ => fst (fold_map (fn (ys, z) => fn i =>
-    ((map (name_thm true) (gen_names i (length ys) name ~~ ys), z), i + length ys)) xs 0));
+fun burrow_fact f = split_list #>> burrow f #> op ~~;
+fun name_thmss name fact = burrow_fact (name_thms true name) fact;
 
 
 (* enter_thms *)