# HG changeset patch
# User wenzelm
# Date 1164769873 -3600
# Node ID ff8062cd41e9d5d40a46fefb7bd66b6e04767c6a
# Parent  abd2b4386a63cb1cb7ea8c80cf9d277538006590
added map/burrow_facts;
exported name_multi, name_thm;

diff -r abd2b4386a63 -r ff8062cd41e9 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Nov 29 04:11:12 2006 +0100
+++ b/src/Pure/pure_thy.ML	Wed Nov 29 04:11:13 2006 +0100
@@ -57,13 +57,17 @@
   val thms_of: theory -> (string * thm) list
   val all_thms_of: theory -> (string * thm) list
   val hide_thms: bool -> string list -> theory -> theory
+  val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
   val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
+  val burrow_facts: ('a list -> 'b list) ->
+    ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
+  val name_multi: string -> 'a list -> (string * 'a) list
+  val name_thm: bool -> string * thm -> thm
   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
   val forall_elim_var: int -> thm -> thm
   val forall_elim_vars: int -> thm -> thm
-  val name_multi: string -> 'a list -> (string * 'a) list
   val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
   val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory 
   val note_thmss: string -> ((bstring * attribute list) *
@@ -308,6 +312,13 @@
   in r := {theorems = (space', thms), index = index}; thy end;
 
 
+(* fact specifications *)
+
+fun map_facts f = map (apsnd (map (apfst (map f))));
+fun burrow_fact f = split_list #>> burrow f #> op ~~;
+fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~;
+
+
 (* naming *)
 
 fun gen_names _ len "" = replicate len ""
@@ -321,7 +332,6 @@
 
 fun name_thms pre name xs = map (name_thm pre) (name_multi name xs);
 
-fun burrow_fact f = split_list #>> burrow f #> op ~~;
 fun name_thmss name fact = burrow_fact (name_thms true name) fact;