src/Pure/Isar/attrib.ML
changeset 30759 3bc78fbb9f57
parent 30575 368e26dfba69
child 30761 ac7570d80c3d
     1.1 --- a/src/Pure/Isar/attrib.ML	Sat Mar 28 17:08:18 2009 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat Mar 28 17:08:49 2009 +0100
     1.3 @@ -18,10 +18,13 @@
     1.4    val attribute_i: theory -> src -> attribute
     1.5    val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
     1.6    val map_specs: ('a -> 'att) ->
     1.7 -    (('c * 'a list) * 'd) list -> (('c * 'att list) * 'd) list
     1.8 +    (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
     1.9    val map_facts: ('a -> 'att) ->
    1.10      (('c * 'a list) * ('d * 'a list) list) list ->
    1.11      (('c * 'att list) * ('d * 'att list) list) list
    1.12 +  val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) ->
    1.13 +    (('c * 'a list) * ('b * 'a list) list) list ->
    1.14 +    (('c * 'att list) * ('fact * 'att list) list) list
    1.15    val crude_closure: Proof.context -> src -> src
    1.16    val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
    1.17    val syntax: attribute context_parser -> src -> attribute
    1.18 @@ -120,15 +123,18 @@
    1.19  
    1.20  fun attribute thy = attribute_i thy o intern_src thy;
    1.21  
    1.22 -fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
    1.23 -    [(Thm.empty_binding, map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
    1.24 +fun eval_thms ctxt args = ProofContext.note_thmss_i Thm.theoremK
    1.25 +    [(Thm.empty_binding, args |> map (fn (a, atts) =>
    1.26 +        (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
    1.27    |> fst |> maps snd;
    1.28  
    1.29  
    1.30  (* attributed declarations *)
    1.31  
    1.32  fun map_specs f = map (apfst (apsnd (map f)));
    1.33 +
    1.34  fun map_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f))));
    1.35 +fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
    1.36  
    1.37  
    1.38  (* crude_closure *)