1.1 --- a/src/Pure/Isar/attrib.ML	Thu Apr 27 12:11:56 2006 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu Apr 27 15:06:35 2006 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4  
     1.5  val thm = gen_thm PureThy.single_thm;
     1.6  val multi_thm = gen_thm (K I);
     1.7 -val thms = Scan.repeat multi_thm >> List.concat;
     1.8 +val thms = Scan.repeat multi_thm >> flat;
     1.9  
    1.10  end;
    1.11  
    1.12 @@ -250,11 +250,11 @@
    1.13      val ctxt = Context.proof_of generic;
    1.14  
    1.15      val (type_insts, term_insts) = List.partition (is_tvar o fst) (map snd mixed_insts);
    1.16 -    val internal_insts = term_insts |> List.mapPartial
    1.17 +    val internal_insts = term_insts |> map_filter
    1.18        (fn (xi, Args.Term t) => SOME (xi, t)
    1.19        | (_, Args.Name _) => NONE
    1.20        | (xi, _) => error_var "Term argument expected for " xi);
    1.21 -    val external_insts = term_insts |> List.mapPartial
    1.22 +    val external_insts = term_insts |> map_filter
    1.23        (fn (xi, Args.Name s) => SOME (xi, s) | _ => NONE);
    1.24  
    1.25