# HG changeset patch
# User wenzelm
# Date 1124356660 -7200
# Node ID 1b07a176a88072d66c3b14f2840cc7d9913b5715
# Parent  89d5bbb2f746d38ab57f736085389f96fcc316cb
added map_specs/facts operators (from locale.ML);

diff -r 89d5bbb2f746 -r 1b07a176a880 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Aug 18 11:17:39 2005 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Aug 18 11:17:40 2005 +0200
@@ -28,6 +28,11 @@
   val context_attribute: ProofContext.context -> Args.src -> ProofContext.context attribute
   val undef_global_attribute: theory attribute
   val undef_local_attribute: ProofContext.context attribute
+  val map_specs: ('a -> 'b attribute) ->
+    (('c * 'a list) * 'd) list -> (('c * 'b attribute list) * 'd) list
+  val map_facts: ('a -> 'b attribute) ->
+    (('c * 'a list) * ('d * 'a list) list) list ->
+    (('c * 'b attribute list) * ('d * 'b attribute list) list) list
   val crude_closure: ProofContext.context -> src -> src
   val add_attributes: (bstring * ((src -> theory attribute) *
       (src -> ProofContext.context attribute)) * string) list -> theory -> theory
@@ -121,6 +126,12 @@
   fn _ => error "attribute undefined in proof context";
 
 
+(* attributed declarations *)
+
+fun map_specs f = map (apfst (apsnd (map f)));
+fun map_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f))));
+
+
 (* crude_closure *)
 
 (*Produce closure without knowing facts in advance! The following