# HG changeset patch
# User wenzelm
# Date 1164560842 -3600
# Node ID 84e98b5f5af0a3415818e3fcce32fc26d91b79aa
# Parent  7140f8aba3801c1414c219be77335131773b63cf
added map_ctxt_attrib;

diff -r 7140f8aba380 -r 84e98b5f5af0 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sun Nov 26 18:07:21 2006 +0100
+++ b/src/Pure/Isar/element.ML	Sun Nov 26 18:07:22 2006 +0100
@@ -25,6 +25,8 @@
     var: string * mixfix -> string * mixfix,
     typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
     attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
+  val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
+    ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
   val morph_ctxt: morphism -> context_i -> context_i
   val params_of: context_i -> (string * typ) list
   val prems_of: context_i -> term list
@@ -109,6 +111,9 @@
    | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
       ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
 
+fun map_ctxt_attrib attrib =
+  map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = attrib};
+
 fun morph_ctxt phi = map_ctxt
  {name = Morphism.name phi,
   var = Morphism.var phi,