Symtab.fold;
authorwenzelm
Fri Jun 17 18:33:29 2005 +0200 (2005-06-17)
changeset 1644480c8f742c6fc
parent 16443 82a116532e3e
child 16445 bc90e58bb6ac
Symtab.fold;
src/Pure/General/name_space.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/General/name_space.ML	Fri Jun 17 18:33:28 2005 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Fri Jun 17 18:33:29 2005 +0200
     1.3 @@ -120,9 +120,8 @@
     1.4    | SOME (name :: _, _) => (name, false)
     1.5    | SOME ([], name' :: _) => (hidden name', true));
     1.6  
     1.7 -fun valid_accesses (NameSpace tab) name =
     1.8 -  ([], tab) |> Symtab.foldl (fn (accs, (xname, (names, _))) =>
     1.9 -    if null names orelse hd names <> name then accs else xname :: accs);
    1.10 +fun valid_accesses (NameSpace tab) name = Symtab.fold (fn (xname, (names, _)) =>
    1.11 +  if not (null names) andalso hd names = name then cons xname else I) tab [];
    1.12  
    1.13  
    1.14  (* intern and extern *)
    1.15 @@ -178,10 +177,9 @@
    1.16  
    1.17  (* merge *)
    1.18  
    1.19 -fun merge (NameSpace tab1, space2) = (space2, tab1) |> Symtab.foldl
    1.20 -  (fn (space, (xname, (names1, names1'))) =>
    1.21 -    map_space (fn (names2, names2') =>
    1.22 -      (merge_lists' names2 names1, merge_lists' names2' names1')) xname space);
    1.23 +fun merge (NameSpace tab1, space2) = Symtab.fold (fn (xname, (names1, names1')) =>
    1.24 +  xname |> map_space (fn (names2, names2') =>
    1.25 +    (merge_lists' names2 names1, merge_lists' names2' names1'))) tab1 space2;
    1.26  
    1.27  
    1.28  (* dest *)
     2.1 --- a/src/Pure/type.ML	Fri Jun 17 18:33:28 2005 +0200
     2.2 +++ b/src/Pure/type.ML	Fri Jun 17 18:33:29 2005 +0200
     2.3 @@ -106,10 +106,8 @@
     2.4  
     2.5  fun build_tsig (classes, default, types, arities) =
     2.6    let
     2.7 -    fun add_log_type (ts, (c, (LogicalType n, _))) = (c, n) :: ts
     2.8 -      | add_log_type (ts, _) = ts;
     2.9      val log_types =
    2.10 -      Symtab.foldl add_log_type ([], #2 types)
    2.11 +      Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (#2 types) []
    2.12        |> Library.sort (Library.int_ord o pairself #2) |> map #1;
    2.13      val witness =
    2.14        (case Sorts.witness_sorts (#2 classes, arities) log_types [] [Graph.keys (#2 classes)] of
    2.15 @@ -440,8 +438,8 @@
    2.16      |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars)
    2.17    in Symtab.update ((t, ars'), arities) end;
    2.18  
    2.19 -fun insert_table pp classes = Symtab.foldl (fn (arities, (t, ars)) =>
    2.20 -  insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars) arities);
    2.21 +fun insert_table pp classes = Symtab.fold (fn (t, ars) =>
    2.22 +  insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars));
    2.23  
    2.24  in
    2.25  
    2.26 @@ -462,10 +460,13 @@
    2.27    in (classes, default, types, arities') end);
    2.28  
    2.29  fun rebuild_arities pp classes arities =
    2.30 -  insert_table pp classes (Symtab.empty, arities);
    2.31 +  Symtab.empty
    2.32 +  |> insert_table pp classes arities;
    2.33  
    2.34  fun merge_arities pp classes (arities1, arities2) =
    2.35 -  insert_table pp classes (insert_table pp classes (Symtab.empty, arities1), arities2);
    2.36 +  Symtab.empty
    2.37 +  |> insert_table pp classes arities1
    2.38 +  |> insert_table pp classes arities2;
    2.39  
    2.40  end;
    2.41