src/Pure/Isar/element.ML
changeset 19482 9f11af8f7ef9
parent 19466 29bc35832a77
child 19585 70a1ce3b23ae
     1.1 --- a/src/Pure/Isar/element.ML	Thu Apr 27 12:11:56 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Thu Apr 27 15:06:35 2006 +0200
     1.3 @@ -100,7 +100,7 @@
     1.4        |> Option.map (fn v => (certT (TVar v), certT T));
     1.5    in
     1.6      Drule.tvars_intr_list (map fst subst) #->
     1.7 -    (fn vs => Thm.instantiate (List.mapPartial (inst vs) subst, []))
     1.8 +    (fn vs => Thm.instantiate (map_filter (inst vs) subst, []))
     1.9    end;
    1.10  
    1.11  fun instantiate_frees thy subst =
    1.12 @@ -144,7 +144,7 @@
    1.13  fun rename_thm ren th =
    1.14    let
    1.15      val subst = Drule.frees_of th
    1.16 -      |> List.mapPartial (fn (x, T) =>
    1.17 +      |> map_filter (fn (x, T) =>
    1.18          let val x' = rename ren x
    1.19          in if x = x' then NONE else SOME ((x, T), (Free (x', T))) end);
    1.20    in
    1.21 @@ -169,7 +169,7 @@
    1.22  
    1.23  fun instT_subst env th =
    1.24    Drule.tfrees_of th
    1.25 -  |> List.mapPartial (fn (a, S) =>
    1.26 +  |> map_filter (fn (a, S) =>
    1.27      let
    1.28        val T = TFree (a, S);
    1.29        val T' = the_default T (Symtab.lookup env a);
    1.30 @@ -209,7 +209,7 @@
    1.31      let
    1.32        val substT = instT_subst envT th;
    1.33        val subst = Drule.frees_of th
    1.34 -        |> List.mapPartial (fn (x, T) =>
    1.35 +        |> map_filter (fn (x, T) =>
    1.36            let
    1.37              val T' = instT_type envT T;
    1.38              val t = Free (x, T');
    1.39 @@ -291,7 +291,7 @@
    1.40        | prt_fact (ths, atts) = Pretty.enclose "(" ")"
    1.41            (Pretty.breaks (map prt_thm ths)) :: Args.pretty_attribs ctxt atts;
    1.42      fun prt_note (a, ths) =
    1.43 -      Pretty.block (Pretty.breaks (List.concat (prt_name_atts a "=" :: map prt_fact ths)));
    1.44 +      Pretty.block (Pretty.breaks (flat (prt_name_atts a "=" :: map prt_fact ths)));
    1.45    in
    1.46      fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes)
    1.47       | Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs)