src/Pure/type.ML
changeset 16444 80c8f742c6fc
parent 16370 033d890fe91f
child 16650 bd4f7149ba1e
     1.1 --- a/src/Pure/type.ML	Fri Jun 17 18:33:28 2005 +0200
     1.2 +++ b/src/Pure/type.ML	Fri Jun 17 18:33:29 2005 +0200
     1.3 @@ -106,10 +106,8 @@
     1.4  
     1.5  fun build_tsig (classes, default, types, arities) =
     1.6    let
     1.7 -    fun add_log_type (ts, (c, (LogicalType n, _))) = (c, n) :: ts
     1.8 -      | add_log_type (ts, _) = ts;
     1.9      val log_types =
    1.10 -      Symtab.foldl add_log_type ([], #2 types)
    1.11 +      Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (#2 types) []
    1.12        |> Library.sort (Library.int_ord o pairself #2) |> map #1;
    1.13      val witness =
    1.14        (case Sorts.witness_sorts (#2 classes, arities) log_types [] [Graph.keys (#2 classes)] of
    1.15 @@ -440,8 +438,8 @@
    1.16      |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars)
    1.17    in Symtab.update ((t, ars'), arities) end;
    1.18  
    1.19 -fun insert_table pp classes = Symtab.foldl (fn (arities, (t, ars)) =>
    1.20 -  insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars) arities);
    1.21 +fun insert_table pp classes = Symtab.fold (fn (t, ars) =>
    1.22 +  insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars));
    1.23  
    1.24  in
    1.25  
    1.26 @@ -462,10 +460,13 @@
    1.27    in (classes, default, types, arities') end);
    1.28  
    1.29  fun rebuild_arities pp classes arities =
    1.30 -  insert_table pp classes (Symtab.empty, arities);
    1.31 +  Symtab.empty
    1.32 +  |> insert_table pp classes arities;
    1.33  
    1.34  fun merge_arities pp classes (arities1, arities2) =
    1.35 -  insert_table pp classes (insert_table pp classes (Symtab.empty, arities1), arities2);
    1.36 +  Symtab.empty
    1.37 +  |> insert_table pp classes arities1
    1.38 +  |> insert_table pp classes arities2;
    1.39  
    1.40  end;
    1.41