src/HOL/Tools/Datatype/datatype_aux.ML
changeset 33244 db230399f890
parent 33243 17014b1b9353
child 33317 b4534348b8fd
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Oct 27 17:34:00 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Oct 27 22:55:27 2009 +0100
     1.3 @@ -255,9 +255,8 @@
     1.4  (* find all non-recursive types in datatype description *)
     1.5  
     1.6  fun get_nonrec_types descr sorts =
     1.7 -  map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) =>
     1.8 -    Library.foldl (fn (Ts', (_, cargs)) =>
     1.9 -      union (op =) (filter_out is_rec_type cargs) Ts') (Ts, constrs)) ([], descr));
    1.10 +  map (typ_of_dtyp descr sorts) (fold (fn (_, (_, _, constrs)) =>
    1.11 +    fold (fn (_, cargs) => union (op =) (filter_out is_rec_type cargs)) constrs) descr []);
    1.12  
    1.13  (* get all recursive types in datatype description *)
    1.14  
    1.15 @@ -335,7 +334,7 @@
    1.16  
    1.17      (* unfold a single constructor argument *)
    1.18  
    1.19 -    fun unfold_arg ((i, Ts, descrs), T) =
    1.20 +    fun unfold_arg T (i, Ts, descrs) =
    1.21        if is_rec_type T then
    1.22          let val (Us, U) = strip_dtyp T
    1.23          in if exists is_rec_type Us then
    1.24 @@ -353,19 +352,17 @@
    1.25  
    1.26      (* unfold a constructor *)
    1.27  
    1.28 -    fun unfold_constr ((i, constrs, descrs), (cname, cargs)) =
    1.29 -      let val (i', cargs', descrs') = Library.foldl unfold_arg ((i, [], descrs), cargs)
    1.30 +    fun unfold_constr (cname, cargs) (i, constrs, descrs) =
    1.31 +      let val (i', cargs', descrs') = fold unfold_arg cargs (i, [], descrs)
    1.32        in (i', constrs @ [(cname, cargs')], descrs') end;
    1.33  
    1.34      (* unfold a single datatype *)
    1.35  
    1.36 -    fun unfold_datatype ((i, dtypes, descrs), (j, (tname, tvars, constrs))) =
    1.37 -      let val (i', constrs', descrs') =
    1.38 -        Library.foldl unfold_constr ((i, [], descrs), constrs)
    1.39 -      in (i', dtypes @ [(j, (tname, tvars, constrs'))], descrs')
    1.40 -      end;
    1.41 +    fun unfold_datatype (j, (tname, tvars, constrs)) (i, dtypes, descrs) =
    1.42 +      let val (i', constrs', descrs') = fold unfold_constr constrs (i, [], descrs)
    1.43 +      in (i', dtypes @ [(j, (tname, tvars, constrs'))], descrs') end;
    1.44  
    1.45 -    val (i', descr', descrs) = Library.foldl unfold_datatype ((i, [],[]), descr);
    1.46 +    val (i', descr', descrs) = fold unfold_datatype descr (i, [], []);
    1.47  
    1.48    in (descr' :: descrs, i') end;
    1.49