--- a/src/Pure/General/graph.ML Sun Jul 08 19:51:55 2007 +0200
+++ b/src/Pure/General/graph.ML Sun Jul 08 19:51:58 2007 +0200
@@ -10,7 +10,6 @@
type key
type 'a T
exception DUP of key
- exception DUPS of key list
exception SAME
exception UNDEF of key
val empty: 'a T
@@ -36,9 +35,9 @@
val is_edge: 'a T -> key * key -> bool
val add_edge: key * key -> 'a T -> 'a T
val del_edge: key * key -> 'a T -> 'a T
- val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception DUPS*)
+ val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception DUP*)
val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
- 'a T * 'a T -> 'a T (*exception DUPS*)
+ 'a T * 'a T -> 'a T (*exception DUP*)
val irreducible_paths: 'a T -> key * key -> key list list
val all_paths: 'a T -> key * key -> key list list
exception CYCLES of key list list
@@ -78,7 +77,6 @@
datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
exception DUP = Table.DUP;
-exception DUPS = Table.DUPS;
exception UNDEF = Table.UNDEF;
exception SAME = Table.SAME;
--- a/src/Pure/General/table.ML Sun Jul 08 19:51:55 2007 +0200
+++ b/src/Pure/General/table.ML Sun Jul 08 19:51:58 2007 +0200
@@ -17,7 +17,6 @@
type key
type 'a table
exception DUP of key
- exception DUPS of key list
exception SAME
exception UNDEF of key
val empty: 'a table
@@ -39,11 +38,11 @@
val default: key * 'a -> 'a table -> 'a table
val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table
- val make: (key * 'a) list -> 'a table (*exception DUPS*)
- val extend: 'a table * (key * 'a) list -> 'a table (*exception DUPS*)
+ val make: (key * 'a) list -> 'a table (*exception DUP*)
+ val extend: 'a table * (key * 'a) list -> 'a table (*exception DUP*)
val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
- 'a table * 'a table -> 'a table (*exception DUPS*)
- val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUPS*)
+ 'a table * 'a table -> 'a table (*exception DUP*)
+ val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUP*)
val delete: key -> 'a table -> 'a table (*exception UNDEF*)
val delete_safe: key -> 'a table -> 'a table
val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool
@@ -56,7 +55,7 @@
val make_list: (key * 'a) list -> 'a list table
val dest_list: 'a list table -> (key * 'a) list
val merge_list: ('a * 'a -> bool) ->
- 'a list table * 'a list table -> 'a list table (*exception DUPS*)
+ 'a list table * 'a list table -> 'a list table (*exception DUP*)
end;
functor TableFun(Key: KEY): TABLE =
@@ -73,7 +72,6 @@
Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;
exception DUP of key;
-exception DUPS of key list;
(* empty *)
@@ -350,23 +348,13 @@
(* simultaneous modifications *)
-fun reject_dups (tab, []) = tab
- | reject_dups (_, dups) = raise DUPS (rev dups);
-
-fun extend (table, args) =
- let
- fun add (key, x) (tab, dups) =
- (update_new (key, x) tab, dups) handle DUP dup => (tab, dup :: dups);
- in reject_dups (fold add args (table, [])) end;
+fun extend (table, args) = fold update_new args table;
fun make entries = extend (empty, entries);
fun join f (table1, table2) =
- let
- fun add (key, y) (tab, dups) =
- let val tab' = modify key (fn NONE => y | SOME x => f key (x, y)) tab
- in (tab', dups) end handle DUP dup => (tab, dup :: dups);
- in reject_dups (fold_table add table2 (table1, [])) end;
+ let fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab;
+ in fold_table add table2 table1 end;
fun merge eq = join (fn key => fn xy => if eq xy then raise SAME else raise DUP key);
--- a/src/Pure/Isar/attrib.ML Sun Jul 08 19:51:55 2007 +0200
+++ b/src/Pure/Isar/attrib.ML Sun Jul 08 19:51:58 2007 +0200
@@ -54,8 +54,8 @@
val empty = NameSpace.empty_table;
val copy = I;
val extend = I;
- fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
- error ("Attempt to merge different versions of attribute(s) " ^ commas_quote dups);
+ fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>
+ error ("Attempt to merge different versions of attribute " ^ quote dup);
);
fun print_attributes thy =
@@ -128,8 +128,7 @@
val new_attrs =
raw_attrs |> map (fn (name, att, comment) => (name, ((att, comment), stamp ())));
fun add attrs = NameSpace.extend_table (Sign.naming_of thy) new_attrs attrs
- handle Symtab.DUPS dups =>
- error ("Duplicate declaration of attributes(s) " ^ commas_quote dups);
+ handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
in AttributesData.map add thy end;
@@ -138,7 +137,7 @@
(* tags *)
-fun tag x = Scan.lift (Args.name -- Scan.repeat Args.name) x;
+fun tag x = Scan.lift (Args.name -- Args.name) x;
(* theorems *)
--- a/src/Pure/Isar/locale.ML Sun Jul 08 19:51:55 2007 +0200
+++ b/src/Pure/Isar/locale.ML Sun Jul 08 19:51:58 2007 +0200
@@ -623,8 +623,8 @@
fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
- handle Symtab.DUPS xs => err_in_locale ctxt
- ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids);
+ handle Symtab.DUP x => err_in_locale ctxt
+ ("Conflicting syntax for parameter: " ^ quote x) (map fst ids);
(* Distinction of assumed vs. derived identifiers.
@@ -722,8 +722,8 @@
fun merge_syn expr syn1 syn2 =
Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
- handle Symtab.DUPS xs => err_in_expr ctxt
- ("Conflicting syntax for parameter(s): " ^ commas_quote xs) expr;
+ handle Symtab.DUP x => err_in_expr ctxt
+ ("Conflicting syntax for parameter: " ^ quote x) expr;
fun params_of (expr as Locale name) =
let
@@ -1063,8 +1063,8 @@
((ids',
merge_syntax ctxt ids'
(syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
- handle Symtab.DUPS xs => err_in_locale ctxt
- ("Conflicting syntax for parameters: " ^ commas_quote xs)
+ handle Symtab.DUP x => err_in_locale ctxt
+ ("Conflicting syntax for parameter: " ^ quote x)
(map #1 ids')),
[((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
end
@@ -2062,9 +2062,9 @@
val eqns' = case get_reg thy_ctxt'' id
of NONE => eqns
| SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
-(* handle Termtab.DUPS ts =>
- error (implode ("Conflicting equations for terms" ::
- map (quote o ProofContext.string_of_term ctxt) ts))
+(* handle Termtab.DUP t =>
+ error (implode ("Conflicting equations for term " ::
+ quote (ProofContext.string_of_term ctxt t)))
*)
in ((id, eqns'), eqns') end;
val all_eqns = fold_map add_eqns all_elemss Termtab.empty |> fst
--- a/src/Pure/Isar/method.ML Sun Jul 08 19:51:55 2007 +0200
+++ b/src/Pure/Isar/method.ML Sun Jul 08 19:51:58 2007 +0200
@@ -389,8 +389,8 @@
val empty = NameSpace.empty_table;
val copy = I;
val extend = I;
- fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
- error ("Attempt to merge different versions of method(s) " ^ commas_quote dups);
+ fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>
+ error ("Attempt to merge different versions of method " ^ quote dup);
);
fun print_methods thy =
@@ -430,8 +430,7 @@
(name, ((f, comment), stamp ())));
fun add meths = NameSpace.extend_table (Sign.naming_of thy) new_meths meths
- handle Symtab.DUPS dups =>
- error ("Duplicate declaration of method(s) " ^ commas_quote dups);
+ handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup);
in MethodsData.map add thy end;
val add_method = add_methods o Library.single;
--- a/src/Pure/Syntax/syntax.ML Sun Jul 08 19:51:55 2007 +0200
+++ b/src/Pure/Syntax/syntax.ML Sun Jul 08 19:51:58 2007 +0200
@@ -98,16 +98,16 @@
fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
-fun err_dup_trfuns name cs =
- error ("More than one " ^ name ^ " for " ^ commas_quote cs);
+fun err_dup_trfun name c =
+ error ("More than one " ^ name ^ " for " ^ quote c);
fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
fun extend_trtab name trfuns tab = Symtab.extend (remove_trtab trfuns tab, trfuns)
- handle Symtab.DUPS cs => err_dup_trfuns name cs;
+ handle Symtab.DUP c => err_dup_trfun name c;
fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
- handle Symtab.DUPS cs => err_dup_trfuns name cs;
+ handle Symtab.DUP c => err_dup_trfun name c;
(* print (ast) translations *)
--- a/src/Pure/Thy/term_style.ML Sun Jul 08 19:51:55 2007 +0200
+++ b/src/Pure/Thy/term_style.ML Sun Jul 08 19:51:58 2007 +0200
@@ -18,8 +18,8 @@
(* style data *)
-fun err_dup_styles names =
- error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
+fun err_dup_style name =
+ error ("Duplicate declaration of antiquote style: " ^ quote name);
structure StyleData = TheoryDataFun
(
@@ -28,7 +28,7 @@
val copy = I;
val extend = I;
fun merge _ tabs : T = Symtab.merge (eq_snd (op =)) tabs
- handle Symtab.DUPS dups => err_dup_styles dups;
+ handle Symtab.DUP dup => err_dup_style dup;
);
fun print_styles thy =
@@ -44,7 +44,7 @@
fun add_style name style thy =
StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy
- handle Symtab.DUP _ => err_dup_styles [name];
+ handle Symtab.DUP _ => err_dup_style name;
(* predefined styles *)
--- a/src/Pure/codegen.ML Sun Jul 08 19:51:55 2007 +0200
+++ b/src/Pure/codegen.ML Sun Jul 08 19:51:58 2007 +0200
@@ -894,7 +894,7 @@
(map (fn s => case Symtab.lookup graphs s of
NONE => error ("Undefined code module: " ^ s)
| SOME gr => gr) modules))
- handle Graph.DUPS ks => error ("Duplicate code for " ^ commas ks);
+ handle Graph.DUP k => error ("Duplicate code for " ^ k);
fun expand (t as Abs _) = t
| expand t = (case fastype_of t of
Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t);
--- a/src/Pure/consts.ML Sun Jul 08 19:51:55 2007 +0200
+++ b/src/Pure/consts.ML Sun Jul 08 19:51:58 2007 +0200
@@ -196,14 +196,14 @@
(** build consts **)
-fun err_dup_consts cs =
- error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
+fun err_dup_const c =
+ error ("Duplicate declaration of constant " ^ quote c);
-fun err_inconsistent_constraints cs =
- error ("Inconsistent type constraints for constant(s) " ^ commas_quote cs);
+fun err_inconsistent_constraints c =
+ error ("Inconsistent type constraints for constant " ^ quote c);
fun extend_decls naming decl tab = NameSpace.extend_table naming [decl] tab
- handle Symtab.DUPS cs => err_dup_consts cs;
+ handle Symtab.DUP c => err_dup_const c;
(* name space *)
@@ -303,9 +303,9 @@
rev_abbrevs = rev_abbrevs2, do_expand = do_expand2}, _)) =
let
val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2)
- handle Symtab.DUPS cs => err_dup_consts cs;
+ handle Symtab.DUP c => err_dup_const c;
val constraints' = Symtab.merge (op =) (constraints1, constraints2)
- handle Symtab.DUPS cs => err_inconsistent_constraints cs;
+ handle Symtab.DUP c => err_inconsistent_constraints c;
val rev_abbrevs' = (rev_abbrevs1, rev_abbrevs2) |> Symtab.join
(K (Library.merge (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u')));
val do_expand' = do_expand1 orelse do_expand2;
--- a/src/Pure/simplifier.ML Sun Jul 08 19:51:55 2007 +0200
+++ b/src/Pure/simplifier.ML Sun Jul 08 19:51:58 2007 +0200
@@ -167,8 +167,7 @@
(** named simprocs **)
-fun err_dup_simprocs ds =
- error ("Duplicate simproc(s): " ^ commas_quote ds);
+fun err_dup_simproc name = error ("Duplicate simproc: " ^ quote name);
(* data *)
@@ -179,7 +178,7 @@
val empty = NameSpace.empty_table;
val extend = I;
fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
- handle Symtab.DUPS ds => err_dup_simprocs ds;
+ handle Symtab.DUP dup => err_dup_simproc dup;
);
@@ -229,7 +228,7 @@
context
|> Simprocs.map (fn simprocs =>
NameSpace.extend_table naming [(name', simproc')] simprocs
- handle Symtab.DUPS ds => err_dup_simprocs ds)
+ handle Symtab.DUP dup => err_dup_simproc dup)
|> map_ss (fn ss => ss addsimprocs [simproc'])
end)
end;
--- 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
--- a/src/Pure/theory.ML Sun Jul 08 19:51:55 2007 +0200
+++ b/src/Pure/theory.ML Sun Jul 08 19:51:58 2007 +0200
@@ -96,8 +96,8 @@
fun make_thy (axioms, defs, oracles) =
Thy {axioms = axioms, defs = defs, oracles = oracles};
-fun err_dup_axms dups = error ("Duplicate axiom(s): " ^ commas_quote dups);
-fun err_dup_oras dups = error ("Duplicate oracle(s): " ^ commas_quote dups);
+fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
+fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
structure ThyData = TheoryDataFun
(
@@ -115,7 +115,7 @@
val axioms = NameSpace.empty_table;
val defs = Defs.merge pp (defs1, defs2);
val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
- handle Symtab.DUPS dups => err_dup_oras dups;
+ handle Symtab.DUP dup => err_dup_ora dup;
in make_thy (axioms, defs, oracles) end;
);
@@ -182,7 +182,7 @@
let
val axms = map (apsnd (Compress.term thy o Logic.varify) o prep_axm thy) raw_axms;
val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms
- handle Symtab.DUPS dups => err_dup_axms dups;
+ handle Symtab.DUP dup => err_dup_axm dup;
in axioms' end);
in
@@ -307,7 +307,7 @@
fun add_oracle (bname, oracle) thy = thy |> map_oracles (fn oracles =>
NameSpace.extend_table (Sign.naming_of thy) [(bname, (oracle, stamp ()))] oracles
- handle Symtab.DUPS dups => err_dup_oras dups);
+ handle Symtab.DUP dup => err_dup_ora dup);
end;
--- a/src/Pure/type.ML Sun Jul 08 19:51:55 2007 +0200
+++ b/src/Pure/type.ML Sun Jul 08 19:51:58 2007 +0200
@@ -570,7 +570,7 @@
fun merge_types (types1, types2) =
NameSpace.merge_tables (Library.eq_snd (op = : serial * serial -> bool)) (types1, types2)
- handle Symtab.DUPS (d :: _) => err_in_decls d (the_decl types1 d) (the_decl types2 d);
+ handle Symtab.DUP d => err_in_decls d (the_decl types1 d) (the_decl types2 d);
end;