# HG changeset patch
# User wenzelm
# Date 896178550 -7200
# Node ID c9c481bc0216a21d3bd5660f6acd7bfb69dcddc9
# Parent  47b8f2d12c53381030ff83f1e051339f6128e771
foldl_map prep_field;

diff -r 47b8f2d12c53 -r c9c481bc0216 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Mon May 25 21:28:07 1998 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue May 26 12:29:10 1998 +0200
@@ -642,15 +642,12 @@
 
     (* fields *)
 
-    fun prep_fields (env, []) = (env, [])
-      | prep_fields (env, (c, raw_T) :: fs) =
-          let
-            val (env', T) = prep_typ sign (env, raw_T) handle ERROR =>
-              error ("The error(s) above occured in field " ^ quote c);
-            val (env'', fs') = prep_fields (env', fs);
-      in (env'', (c, T) :: fs') end;
+    fun prep_field (env, (c, raw_T)) =
+      let val (env', T) = prep_typ sign (env, raw_T) handle ERROR =>
+        error ("The error(s) above occured in field " ^ quote c)
+      in (env', (c, T)) end;
 
-    val (envir, bfields) = prep_fields (init_env, raw_fields);
+    val (envir, bfields) = foldl_map prep_field (init_env, raw_fields);
     val envir_names = map fst envir;