diff -r 3633f560f4c3 -r 479806475f3c src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sun Mar 01 16:48:06 2009 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Sun Mar 01 23:36:12 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Tools/datatype_package.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
@@ -140,11 +139,11 @@
   (*Treatment of a list of constructors, for one part
     Result adds a list of terms, each a function variable with arguments*)
   fun add_case_list (con_ty_list, (opno, case_lists)) =
-    let val (opno', case_list) = foldr add_case (opno, []) con_ty_list
+    let val (opno', case_list) = List.foldr add_case (opno, []) con_ty_list
     in (opno', case_list :: case_lists) end;
 
   (*Treatment of all parts*)
-  val (_, case_lists) = foldr add_case_list (1,[]) con_ty_lists;
+  val (_, case_lists) = List.foldr add_case_list (1,[]) con_ty_lists;
 
   (*extract the types of all the variables*)
   val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) ---> @{typ "i => i"};
@@ -184,7 +183,7 @@
           val rec_args = map (make_rec_call (rev case_args,0))
                          (List.drop(recursor_args, ncase_args))
       in
-          foldr add_abs
+          List.foldr add_abs
             (list_comb (recursor_var,
                         bound_args @ rec_args)) case_args
       end
@@ -216,7 +215,7 @@
   val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists);
 
   (*Treatment of all parts*)
-  val (_, recursor_lists) = foldr add_case_list (1,[]) rec_ty_lists;
+  val (_, recursor_lists) = List.foldr add_case_list (1,[]) rec_ty_lists;
 
   (*extract the types of all the variables*)
   val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists) ---> @{typ "i => i"};