# HG changeset patch
# User wenzelm
# Date 1208360441 -7200
# Node ID 40aefd1e8f05ac103101d2970fff2e641a00b3c4
# Parent  0701201def955b5b3ca9d35ac965bf84cb3f738d
PureThy.get_fact: pass dynamic context;

diff -r 0701201def95 -r 40aefd1e8f05 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Apr 16 17:40:40 2008 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed Apr 16 17:40:41 2008 +0200
@@ -107,8 +107,8 @@
 fun attribute thy = attribute_i thy o intern_src thy;
 
 fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
-  [(("", []), map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
-  |> (flat o map snd o fst);
+    [(("", []), map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
+  |> fst |> maps snd;
 
 
 (* attributed declarations *)
@@ -162,7 +162,7 @@
 fun gen_thm pick = Scan.depend (fn context =>
   let
     val thy = Context.theory_of context;
-    val get = Context.cases PureThy.get_fact ProofContext.get_fact context;
+    val get = Context.cases (PureThy.get_fact context) ProofContext.get_fact context;
     val get_fact = get o Facts.Fact;
     val get_named = get o Facts.named;
   in