src/HOL/Tools/inductive_realizer.ML
changeset 32952 aeb1e44fbc19
parent 32131 7913823f14e3
child 33040 cffdb7b28498
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Oct 15 23:10:35 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Oct 15 23:28:10 2009 +0200
     1.3 @@ -225,7 +225,7 @@
     1.4          let
     1.5            val Type ("fun", [U, _]) = T;
     1.6            val a :: names' = names
     1.7 -        in (list_abs_free (("x", U) :: List.mapPartial (fn intr =>
     1.8 +        in (list_abs_free (("x", U) :: map_filter (fn intr =>
     1.9            Option.map (pair (name_of_fn intr))
    1.10              (AList.lookup (op =) frees (name_of_fn intr))) intrs,
    1.11            list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
    1.12 @@ -300,7 +300,7 @@
    1.13        fold (fn s => AxClass.axiomatize_arity
    1.14          (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
    1.15          Extraction.add_typeof_eqns_i ty_eqs;
    1.16 -    val dts = List.mapPartial (fn (s, rs) => if s mem rsets then
    1.17 +    val dts = map_filter (fn (s, rs) => if s mem rsets then
    1.18        SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
    1.19  
    1.20      (** datatype representing computational content of inductive set **)
    1.21 @@ -332,7 +332,7 @@
    1.22        (Extraction.realizes_of thy2 vs
    1.23          (if c = Extraction.nullt then c else list_comb (c, map Var (rev
    1.24            (Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
    1.25 -            (maps snd rss ~~ List.concat constrss);
    1.26 +            (maps snd rss ~~ flat constrss);
    1.27      val (rlzpreds, rlzpreds') =
    1.28        rintrs |> map (fn rintr =>
    1.29          let
    1.30 @@ -470,9 +470,8 @@
    1.31        (map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
    1.32           (name_of_thm rule, rule, rrule, rlz,
    1.33              list_comb (c, map Var (rev (Term.add_vars (prop_of rule) []) \\ params'))))
    1.34 -              (List.concat (map snd rss) ~~ #intrs ind_info ~~ rintrs ~~
    1.35 -                 List.concat constrss))) thy4;
    1.36 -    val elimps = List.mapPartial (fn ((s, intrs), p) =>
    1.37 +              (maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4;
    1.38 +    val elimps = map_filter (fn ((s, intrs), p) =>
    1.39        if s mem rsets then SOME (p, intrs) else NONE)
    1.40          (rss' ~~ (elims ~~ #elims ind_info));
    1.41      val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>