src/Pure/Isar/element.ML
changeset 21528 84e98b5f5af0
parent 21521 095f4963beed
child 21581 7799b1739a51
     1.1 --- a/src/Pure/Isar/element.ML	Sun Nov 26 18:07:21 2006 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Sun Nov 26 18:07:22 2006 +0100
     1.3 @@ -25,6 +25,8 @@
     1.4      var: string * mixfix -> string * mixfix,
     1.5      typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
     1.6      attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
     1.7 +  val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
     1.8 +    ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
     1.9    val morph_ctxt: morphism -> context_i -> context_i
    1.10    val params_of: context_i -> (string * typ) list
    1.11    val prems_of: context_i -> term list
    1.12 @@ -109,6 +111,9 @@
    1.13     | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
    1.14        ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
    1.15  
    1.16 +fun map_ctxt_attrib attrib =
    1.17 +  map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = attrib};
    1.18 +
    1.19  fun morph_ctxt phi = map_ctxt
    1.20   {name = Morphism.name phi,
    1.21    var = Morphism.var phi,