src/Pure/Isar/obtain.ML
changeset 19482 9f11af8f7ef9
parent 19300 7689f81f8996
child 19585 70a1ce3b23ae
     1.1 --- a/src/Pure/Isar/obtain.ML	Thu Apr 27 12:11:56 2006 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Thu Apr 27 15:06:35 2006 +0200
     1.3 @@ -119,7 +119,7 @@
     1.4  
     1.5      (*obtain asms*)
     1.6      val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
     1.7 -    val asm_props = List.concat (map (map fst) proppss);
     1.8 +    val asm_props = maps (map fst) proppss;
     1.9      val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
    1.10  
    1.11      val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
    1.12 @@ -131,9 +131,9 @@
    1.13      fun occs_var x = Library.get_first (fn t =>
    1.14        Term.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
    1.15      val raw_parms = map occs_var xs;
    1.16 -    val parms = List.mapPartial I raw_parms;
    1.17 +    val parms = map_filter I raw_parms;
    1.18      val parm_names =
    1.19 -      List.mapPartial (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs);
    1.20 +      map_filter (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs);
    1.21  
    1.22      val that_name = if name = "" then thatN else name;
    1.23      val that_prop =
    1.24 @@ -284,7 +284,7 @@
    1.25      val names =
    1.26        cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name);
    1.27      val elems = cases |> map (fn (_, (vars, _)) =>
    1.28 -      Element.Constrains (vars |> List.mapPartial (fn (x, SOME T) => SOME (x, T) | _ => NONE)));
    1.29 +      Element.Constrains (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE)));
    1.30      val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair ([], [])) props));
    1.31  
    1.32      fun mk_stmt stmt ctxt =