1.1 --- a/src/Pure/Isar/attrib.ML	Wed Apr 16 17:40:40 2008 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Wed Apr 16 17:40:41 2008 +0200
     1.3 @@ -107,8 +107,8 @@
     1.4  fun attribute thy = attribute_i thy o intern_src thy;
     1.5  
     1.6  fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
     1.7 -  [(("", []), map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
     1.8 -  |> (flat o map snd o fst);
     1.9 +    [(("", []), map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
    1.10 +  |> fst |> maps snd;
    1.11  
    1.12  
    1.13  (* attributed declarations *)
    1.14 @@ -162,7 +162,7 @@
    1.15  fun gen_thm pick = Scan.depend (fn context =>
    1.16    let
    1.17      val thy = Context.theory_of context;
    1.18 -    val get = Context.cases PureThy.get_fact ProofContext.get_fact context;
    1.19 +    val get = Context.cases (PureThy.get_fact context) ProofContext.get_fact context;
    1.20      val get_fact = get o Facts.Fact;
    1.21      val get_named = get o Facts.named;
    1.22    in