src/Pure/Isar/attrib.ML
changeset 45390 e29521ef9059
parent 45375 7fe19930dfc9
child 45491 3c9aff74fb58
     1.1 --- a/src/Pure/Isar/attrib.ML	Mon Nov 07 16:41:16 2011 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Mon Nov 07 17:00:23 2011 +0100
     1.3 @@ -16,12 +16,12 @@
     1.4    val defined: theory -> string -> bool
     1.5    val attribute: theory -> src -> attribute
     1.6    val attribute_i: theory -> src -> attribute
     1.7 -  val map_specs: ('a -> 'att) ->
     1.8 +  val map_specs: ('a list -> 'att list) ->
     1.9      (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
    1.10 -  val map_facts: ('a -> 'att) ->
    1.11 +  val map_facts: ('a list -> 'att list) ->
    1.12      (('c * 'a list) * ('d * 'a list) list) list ->
    1.13      (('c * 'att list) * ('d * 'att list) list) list
    1.14 -  val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) ->
    1.15 +  val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
    1.16      (('c * 'a list) * ('b * 'a list) list) list ->
    1.17      (('c * 'att list) * ('fact * 'att list) list) list
    1.18    val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
    1.19 @@ -127,9 +127,9 @@
    1.20  
    1.21  (* attributed declarations *)
    1.22  
    1.23 -fun map_specs f = map (apfst (apsnd (map f)));
    1.24 +fun map_specs f = map (apfst (apsnd f));
    1.25  
    1.26 -fun map_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f))));
    1.27 +fun map_facts f = map (apfst (apsnd f) o apsnd (map (apsnd f)));
    1.28  fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
    1.29  
    1.30  
    1.31 @@ -137,7 +137,7 @@
    1.32  
    1.33  fun eval_thms ctxt srcs = ctxt
    1.34    |> Proof_Context.note_thmss ""
    1.35 -    (map_facts_refs (attribute (Proof_Context.theory_of ctxt)) (Proof_Context.get_fact ctxt)
    1.36 +    (map_facts_refs (map (attribute (Proof_Context.theory_of ctxt))) (Proof_Context.get_fact ctxt)
    1.37        [((Binding.empty, []), srcs)])
    1.38    |> fst |> maps snd;
    1.39