src/HOL/Tools/record.ML
changeset 32952 aeb1e44fbc19
parent 32809 e72347dd3e64
child 32957 675c0c7e6a37
child 33053 dabf9d1bb552
     1.1 --- a/src/HOL/Tools/record.ML	Thu Oct 15 23:10:35 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Thu Oct 15 23:28:10 2009 +0200
     1.3 @@ -656,7 +656,7 @@
     1.4  
     1.5          fun bad_inst ((x, S), T) =
     1.6            if Sign.of_sort thy (T, S) then NONE else SOME x
     1.7 -        val bads = List.mapPartial bad_inst (args ~~ types);
     1.8 +        val bads = map_filter bad_inst (args ~~ types);
     1.9          val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");
    1.10  
    1.11          val inst = map fst args ~~ types;
    1.12 @@ -1362,7 +1362,7 @@
    1.13            | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _) => x) us);
    1.14  
    1.15          val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
    1.16 -        val noops' = flat (map snd (Symtab.dest noops));
    1.17 +        val noops' = maps snd (Symtab.dest noops);
    1.18        in
    1.19          if simp then
    1.20            SOME
    1.21 @@ -1521,7 +1521,7 @@
    1.22                end)
    1.23        | split_free_tac _ _ _ = NONE;
    1.24  
    1.25 -    val split_frees_tacs = List.mapPartial (split_free_tac P i) frees;
    1.26 +    val split_frees_tacs = map_filter (split_free_tac P i) frees;
    1.27  
    1.28      val simprocs = if has_rec goal then [record_split_simproc P] else [];
    1.29      val thms' = K_comp_convs @ thms;
    1.30 @@ -1860,7 +1860,7 @@
    1.31      val (bfields, field_syntax) =
    1.32        split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
    1.33  
    1.34 -    val parent_fields = List.concat (map #fields parents);
    1.35 +    val parent_fields = maps #fields parents;
    1.36      val parent_chunks = map (length o #fields) parents;
    1.37      val parent_names = map fst parent_fields;
    1.38      val parent_types = map snd parent_fields;