--- a/src/Pure/sorts.ML Sun Jul 08 19:51:55 2007 +0200
+++ b/src/Pure/sorts.ML Sun Jul 08 19:51:58 2007 +0200
@@ -183,8 +183,7 @@
(* classes *)
-fun err_dup_classes cs =
- error ("Duplicate declaration of class(es): " ^ commas_quote cs);
+fun err_dup_class c = error ("Duplicate declaration of class: " ^ quote c);
fun err_cyclic_classes pp css =
error (cat_lines (map (fn cs =>
@@ -193,7 +192,7 @@
fun add_class pp (c, cs) = map_classes (fn classes =>
let
val classes' = classes |> Graph.new_node (c, serial ())
- handle Graph.DUP dup => err_dup_classes [dup];
+ handle Graph.DUP dup => err_dup_class dup;
val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs)
handle Graph.CYCLES css => err_cyclic_classes pp css;
in classes'' end);
@@ -274,7 +273,7 @@
Algebra {classes = classes2, arities = arities2}) =
let
val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2)
- handle Graph.DUPS cs => err_dup_classes cs
+ handle Graph.DUP c => err_dup_class c
| Graph.CYCLES css => err_cyclic_classes pp css;
val algebra0 = make_algebra (classes', Symtab.empty);
val arities' = Symtab.empty