# HG changeset patch
# User wenzelm
# Date 1281540297 -7200
# Node ID e98236e5068b2c492e9b7a2801259ad129e633b8
# Parent  16bb1e60204b2b1c76efbd0c1ce94d5f16ce22da
tuned eval_thms (cf. note etc. in proof.ML);

diff -r 16bb1e60204b -r e98236e5068b src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Aug 11 15:17:13 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed Aug 11 17:24:57 2010 +0200
@@ -16,7 +16,6 @@
   val defined: theory -> string -> bool
   val attribute: theory -> src -> attribute
   val attribute_i: theory -> src -> attribute
-  val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
   val map_specs: ('a -> 'att) ->
     (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
   val map_facts: ('a -> 'att) ->
@@ -25,6 +24,7 @@
   val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) ->
     (('c * 'a list) * ('b * 'a list) list) list ->
     (('c * 'att list) * ('fact * 'att list) list) list
+  val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
   val crude_closure: Proof.context -> src -> src
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
   val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
@@ -114,11 +114,6 @@
 
 fun attribute thy = attribute_i thy o intern_src thy;
 
-fun eval_thms ctxt args = ProofContext.note_thmss ""
-    [(Thm.empty_binding, args |> map (fn (a, atts) =>
-        (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
-  |> fst |> maps snd;
-
 
 (* attributed declarations *)
 
@@ -128,6 +123,15 @@
 fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
 
 
+(* fact expressions *)
+
+fun eval_thms ctxt srcs = ctxt
+  |> ProofContext.note_thmss ""
+    (map_facts_refs (attribute (ProofContext.theory_of ctxt)) (ProofContext.get_fact ctxt)
+      [((Binding.empty, []), srcs)])
+  |> fst |> maps snd;
+
+
 (* crude_closure *)
 
 (*Produce closure without knowing facts in advance! The following