tuned eval_thms (cf. note etc. in proof.ML);
authorwenzelm
Wed Aug 11 17:24:57 2010 +0200 (2010-08-11 ago)
changeset 38330e98236e5068b
parent 38329 16bb1e60204b
child 38331 6e72f31999ac
tuned eval_thms (cf. note etc. in proof.ML);
src/Pure/Isar/attrib.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Wed Aug 11 15:17:13 2010 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Wed Aug 11 17:24:57 2010 +0200
     1.3 @@ -16,7 +16,6 @@
     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 eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
     1.8    val map_specs: ('a -> 'att) ->
     1.9      (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
    1.10    val map_facts: ('a -> 'att) ->
    1.11 @@ -25,6 +24,7 @@
    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 eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
    1.16    val crude_closure: Proof.context -> src -> src
    1.17    val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
    1.18    val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
    1.19 @@ -114,11 +114,6 @@
    1.20  
    1.21  fun attribute thy = attribute_i thy o intern_src thy;
    1.22  
    1.23 -fun eval_thms ctxt args = ProofContext.note_thmss ""
    1.24 -    [(Thm.empty_binding, args |> map (fn (a, atts) =>
    1.25 -        (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
    1.26 -  |> fst |> maps snd;
    1.27 -
    1.28  
    1.29  (* attributed declarations *)
    1.30  
    1.31 @@ -128,6 +123,15 @@
    1.32  fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
    1.33  
    1.34  
    1.35 +(* fact expressions *)
    1.36 +
    1.37 +fun eval_thms ctxt srcs = ctxt
    1.38 +  |> ProofContext.note_thmss ""
    1.39 +    (map_facts_refs (attribute (ProofContext.theory_of ctxt)) (ProofContext.get_fact ctxt)
    1.40 +      [((Binding.empty, []), srcs)])
    1.41 +  |> fst |> maps snd;
    1.42 +
    1.43 +
    1.44  (* crude_closure *)
    1.45  
    1.46  (*Produce closure without knowing facts in advance! The following