Symtab.fold;

--- a/src/Pure/General/name_space.ML	Fri Jun 17 18:33:28 2005 +0200
+++ b/src/Pure/General/name_space.ML	Fri Jun 17 18:33:29 2005 +0200
@@ -120,9 +120,8 @@
   | SOME (name :: _, _) => (name, false)
   | SOME ([], name' :: _) => (hidden name', true));
 
-fun valid_accesses (NameSpace tab) name =
-  ([], tab) |> Symtab.foldl (fn (accs, (xname, (names, _))) =>
-    if null names orelse hd names <> name then accs else xname :: accs);
+fun valid_accesses (NameSpace tab) name = Symtab.fold (fn (xname, (names, _)) =>
+  if not (null names) andalso hd names = name then cons xname else I) tab [];
 
 
 (* intern and extern *)
@@ -178,10 +177,9 @@
 
 (* merge *)
 
-fun merge (NameSpace tab1, space2) = (space2, tab1) |> Symtab.foldl
-  (fn (space, (xname, (names1, names1'))) =>
-    map_space (fn (names2, names2') =>
-      (merge_lists' names2 names1, merge_lists' names2' names1')) xname space);
+fun merge (NameSpace tab1, space2) = Symtab.fold (fn (xname, (names1, names1')) =>
+  xname |> map_space (fn (names2, names2') =>
+    (merge_lists' names2 names1, merge_lists' names2' names1'))) tab1 space2;
 
 
 (* dest *)

--- a/src/Pure/type.ML	Fri Jun 17 18:33:28 2005 +0200
+++ b/src/Pure/type.ML	Fri Jun 17 18:33:29 2005 +0200
@@ -106,10 +106,8 @@
 
 fun build_tsig (classes, default, types, arities) =
   let
-    fun add_log_type (ts, (c, (LogicalType n, _))) = (c, n) :: ts
-      | add_log_type (ts, _) = ts;
     val log_types =
-      Symtab.foldl add_log_type ([], #2 types)
+      Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (#2 types) []
       |> Library.sort (Library.int_ord o pairself #2) |> map #1;
     val witness =
       (case Sorts.witness_sorts (#2 classes, arities) log_types [] [Graph.keys (#2 classes)] of
@@ -440,8 +438,8 @@
     |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars)
   in Symtab.update ((t, ars'), arities) end;
 
-fun insert_table pp classes = Symtab.foldl (fn (arities, (t, ars)) =>
-  insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars) arities);
+fun insert_table pp classes = Symtab.fold (fn (t, ars) =>
+  insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars));
 
 in
 
@@ -462,10 +460,13 @@
   in (classes, default, types, arities') end);
 
 fun rebuild_arities pp classes arities =
-  insert_table pp classes (Symtab.empty, arities);
+  Symtab.empty
+  |> insert_table pp classes arities;
 
 fun merge_arities pp classes (arities1, arities2) =
-  insert_table pp classes (insert_table pp classes (Symtab.empty, arities1), arities2);
+  Symtab.empty
+  |> insert_table pp classes arities1
+  |> insert_table pp classes arities2;
 
 end;