1.1 --- a/src/HOL/Tools/record_package.ML	Mon May 25 21:28:07 1998 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Tue May 26 12:29:10 1998 +0200
     1.3 @@ -642,15 +642,12 @@
     1.4  
     1.5      (* fields *)
     1.6  
     1.7 -    fun prep_fields (env, []) = (env, [])
     1.8 -      | prep_fields (env, (c, raw_T) :: fs) =
     1.9 -          let
    1.10 -            val (env', T) = prep_typ sign (env, raw_T) handle ERROR =>
    1.11 -              error ("The error(s) above occured in field " ^ quote c);
    1.12 -            val (env'', fs') = prep_fields (env', fs);
    1.13 -      in (env'', (c, T) :: fs') end;
    1.14 +    fun prep_field (env, (c, raw_T)) =
    1.15 +      let val (env', T) = prep_typ sign (env, raw_T) handle ERROR =>
    1.16 +        error ("The error(s) above occured in field " ^ quote c)
    1.17 +      in (env', (c, T)) end;
    1.18  
    1.19 -    val (envir, bfields) = prep_fields (init_env, raw_fields);
    1.20 +    val (envir, bfields) = foldl_map prep_field (init_env, raw_fields);
    1.21      val envir_names = map fst envir;
    1.22  
    1.23