replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
authorwenzelm
Sun Jul 08 19:51:58 2007 +0200 (2007-07-08)
changeset 23655d2d1138e0ddc
parent 23654 a2ad1c166ac8
child 23656 4bdcb024e95d
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
src/Pure/General/graph.ML
src/Pure/General/table.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Syntax/syntax.ML
src/Pure/Thy/term_style.ML
src/Pure/codegen.ML
src/Pure/consts.ML
src/Pure/simplifier.ML
src/Pure/sorts.ML
src/Pure/theory.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/General/graph.ML	Sun Jul 08 19:51:55 2007 +0200
     1.2 +++ b/src/Pure/General/graph.ML	Sun Jul 08 19:51:58 2007 +0200
     1.3 @@ -10,7 +10,6 @@
     1.4    type key
     1.5    type 'a T
     1.6    exception DUP of key
     1.7 -  exception DUPS of key list
     1.8    exception SAME
     1.9    exception UNDEF of key
    1.10    val empty: 'a T
    1.11 @@ -36,9 +35,9 @@
    1.12    val is_edge: 'a T -> key * key -> bool
    1.13    val add_edge: key * key -> 'a T -> 'a T
    1.14    val del_edge: key * key -> 'a T -> 'a T
    1.15 -  val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUPS*)
    1.16 +  val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUP*)
    1.17    val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
    1.18 -    'a T * 'a T -> 'a T                                               (*exception DUPS*)
    1.19 +    'a T * 'a T -> 'a T                                               (*exception DUP*)
    1.20    val irreducible_paths: 'a T -> key * key -> key list list
    1.21    val all_paths: 'a T -> key * key -> key list list
    1.22    exception CYCLES of key list list
    1.23 @@ -78,7 +77,6 @@
    1.24  datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
    1.25  
    1.26  exception DUP = Table.DUP;
    1.27 -exception DUPS = Table.DUPS;
    1.28  exception UNDEF = Table.UNDEF;
    1.29  exception SAME = Table.SAME;
    1.30  
     2.1 --- a/src/Pure/General/table.ML	Sun Jul 08 19:51:55 2007 +0200
     2.2 +++ b/src/Pure/General/table.ML	Sun Jul 08 19:51:58 2007 +0200
     2.3 @@ -17,7 +17,6 @@
     2.4    type key
     2.5    type 'a table
     2.6    exception DUP of key
     2.7 -  exception DUPS of key list
     2.8    exception SAME
     2.9    exception UNDEF of key
    2.10    val empty: 'a table
    2.11 @@ -39,11 +38,11 @@
    2.12    val default: key * 'a -> 'a table -> 'a table
    2.13    val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
    2.14    val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table
    2.15 -  val make: (key * 'a) list -> 'a table                                (*exception DUPS*)
    2.16 -  val extend: 'a table * (key * 'a) list -> 'a table                   (*exception DUPS*)
    2.17 +  val make: (key * 'a) list -> 'a table                                (*exception DUP*)
    2.18 +  val extend: 'a table * (key * 'a) list -> 'a table                   (*exception DUP*)
    2.19    val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
    2.20 -    'a table * 'a table -> 'a table                                    (*exception DUPS*)
    2.21 -  val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table      (*exception DUPS*)
    2.22 +    'a table * 'a table -> 'a table                                    (*exception DUP*)
    2.23 +  val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table      (*exception DUP*)
    2.24    val delete: key -> 'a table -> 'a table                              (*exception UNDEF*)
    2.25    val delete_safe: key -> 'a table -> 'a table
    2.26    val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool
    2.27 @@ -56,7 +55,7 @@
    2.28    val make_list: (key * 'a) list -> 'a list table
    2.29    val dest_list: 'a list table -> (key * 'a) list
    2.30    val merge_list: ('a * 'a -> bool) ->
    2.31 -    'a list table * 'a list table -> 'a list table                     (*exception DUPS*)
    2.32 +    'a list table * 'a list table -> 'a list table                     (*exception DUP*)
    2.33  end;
    2.34  
    2.35  functor TableFun(Key: KEY): TABLE =
    2.36 @@ -73,7 +72,6 @@
    2.37    Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;
    2.38  
    2.39  exception DUP of key;
    2.40 -exception DUPS of key list;
    2.41  
    2.42  
    2.43  (* empty *)
    2.44 @@ -350,23 +348,13 @@
    2.45  
    2.46  (* simultaneous modifications *)
    2.47  
    2.48 -fun reject_dups (tab, []) = tab
    2.49 -  | reject_dups (_, dups) = raise DUPS (rev dups);
    2.50 -
    2.51 -fun extend (table, args) =
    2.52 -  let
    2.53 -    fun add (key, x) (tab, dups) =
    2.54 -      (update_new (key, x) tab, dups) handle DUP dup => (tab, dup :: dups);
    2.55 -  in reject_dups (fold add args (table, [])) end;
    2.56 +fun extend (table, args) = fold update_new args table;
    2.57  
    2.58  fun make entries = extend (empty, entries);
    2.59  
    2.60  fun join f (table1, table2) =
    2.61 -  let
    2.62 -    fun add (key, y) (tab, dups) =
    2.63 -      let val tab' = modify key (fn NONE => y | SOME x => f key (x, y)) tab
    2.64 -      in (tab', dups) end handle DUP dup => (tab, dup :: dups);
    2.65 -  in reject_dups (fold_table add table2 (table1, [])) end;
    2.66 +  let fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab;
    2.67 +  in fold_table add table2 table1 end;
    2.68  
    2.69  fun merge eq = join (fn key => fn xy => if eq xy then raise SAME else raise DUP key);
    2.70  
     3.1 --- a/src/Pure/Isar/attrib.ML	Sun Jul 08 19:51:55 2007 +0200
     3.2 +++ b/src/Pure/Isar/attrib.ML	Sun Jul 08 19:51:58 2007 +0200
     3.3 @@ -54,8 +54,8 @@
     3.4    val empty = NameSpace.empty_table;
     3.5    val copy = I;
     3.6    val extend = I;
     3.7 -  fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
     3.8 -    error ("Attempt to merge different versions of attribute(s) " ^ commas_quote dups);
     3.9 +  fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>
    3.10 +    error ("Attempt to merge different versions of attribute " ^ quote dup);
    3.11  );
    3.12  
    3.13  fun print_attributes thy =
    3.14 @@ -128,8 +128,7 @@
    3.15      val new_attrs =
    3.16        raw_attrs |> map (fn (name, att, comment) => (name, ((att, comment), stamp ())));
    3.17      fun add attrs = NameSpace.extend_table (Sign.naming_of thy) new_attrs attrs
    3.18 -      handle Symtab.DUPS dups =>
    3.19 -        error ("Duplicate declaration of attributes(s) " ^ commas_quote dups);
    3.20 +      handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
    3.21    in AttributesData.map add thy end;
    3.22  
    3.23  
    3.24 @@ -138,7 +137,7 @@
    3.25  
    3.26  (* tags *)
    3.27  
    3.28 -fun tag x = Scan.lift (Args.name -- Scan.repeat Args.name) x;
    3.29 +fun tag x = Scan.lift (Args.name -- Args.name) x;
    3.30  
    3.31  
    3.32  (* theorems *)
     4.1 --- a/src/Pure/Isar/locale.ML	Sun Jul 08 19:51:55 2007 +0200
     4.2 +++ b/src/Pure/Isar/locale.ML	Sun Jul 08 19:51:58 2007 +0200
     4.3 @@ -623,8 +623,8 @@
     4.4  
     4.5  
     4.6  fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
     4.7 -  handle Symtab.DUPS xs => err_in_locale ctxt
     4.8 -    ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids);
     4.9 +  handle Symtab.DUP x => err_in_locale ctxt
    4.10 +    ("Conflicting syntax for parameter: " ^ quote x) (map fst ids);
    4.11  
    4.12  
    4.13  (* Distinction of assumed vs. derived identifiers.
    4.14 @@ -722,8 +722,8 @@
    4.15  
    4.16      fun merge_syn expr syn1 syn2 =
    4.17          Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
    4.18 -        handle Symtab.DUPS xs => err_in_expr ctxt
    4.19 -          ("Conflicting syntax for parameter(s): " ^ commas_quote xs) expr;
    4.20 +        handle Symtab.DUP x => err_in_expr ctxt
    4.21 +          ("Conflicting syntax for parameter: " ^ quote x) expr;
    4.22  
    4.23      fun params_of (expr as Locale name) =
    4.24            let
    4.25 @@ -1063,8 +1063,8 @@
    4.26          ((ids',
    4.27           merge_syntax ctxt ids'
    4.28             (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
    4.29 -           handle Symtab.DUPS xs => err_in_locale ctxt
    4.30 -             ("Conflicting syntax for parameters: " ^ commas_quote xs)
    4.31 +           handle Symtab.DUP x => err_in_locale ctxt
    4.32 +             ("Conflicting syntax for parameter: " ^ quote x)
    4.33               (map #1 ids')),
    4.34           [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
    4.35        end
    4.36 @@ -2062,9 +2062,9 @@
    4.37           val eqns' = case get_reg thy_ctxt'' id
    4.38             of NONE => eqns
    4.39              | SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
    4.40 -(*                handle Termtab.DUPS ts =>
    4.41 -                  error (implode ("Conflicting equations for terms" ::
    4.42 -                    map (quote o ProofContext.string_of_term ctxt) ts))
    4.43 +(*                handle Termtab.DUP t =>
    4.44 +                  error (implode ("Conflicting equations for term " ::
    4.45 +                    quote (ProofContext.string_of_term ctxt t)))
    4.46  *)
    4.47         in ((id, eqns'), eqns') end;
    4.48      val all_eqns = fold_map add_eqns all_elemss Termtab.empty |> fst
     5.1 --- a/src/Pure/Isar/method.ML	Sun Jul 08 19:51:55 2007 +0200
     5.2 +++ b/src/Pure/Isar/method.ML	Sun Jul 08 19:51:58 2007 +0200
     5.3 @@ -389,8 +389,8 @@
     5.4    val empty = NameSpace.empty_table;
     5.5    val copy = I;
     5.6    val extend = I;
     5.7 -  fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
     5.8 -    error ("Attempt to merge different versions of method(s) " ^ commas_quote dups);
     5.9 +  fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>
    5.10 +    error ("Attempt to merge different versions of method " ^ quote dup);
    5.11  );
    5.12  
    5.13  fun print_methods thy =
    5.14 @@ -430,8 +430,7 @@
    5.15        (name, ((f, comment), stamp ())));
    5.16  
    5.17      fun add meths = NameSpace.extend_table (Sign.naming_of thy) new_meths meths
    5.18 -      handle Symtab.DUPS dups =>
    5.19 -        error ("Duplicate declaration of method(s) " ^ commas_quote dups);
    5.20 +      handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup);
    5.21    in MethodsData.map add thy end;
    5.22  
    5.23  val add_method = add_methods o Library.single;
     6.1 --- a/src/Pure/Syntax/syntax.ML	Sun Jul 08 19:51:55 2007 +0200
     6.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Jul 08 19:51:58 2007 +0200
     6.3 @@ -98,16 +98,16 @@
     6.4  
     6.5  fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
     6.6  
     6.7 -fun err_dup_trfuns name cs =
     6.8 -  error ("More than one " ^ name ^ " for " ^ commas_quote cs);
     6.9 +fun err_dup_trfun name c =
    6.10 +  error ("More than one " ^ name ^ " for " ^ quote c);
    6.11  
    6.12  fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
    6.13  
    6.14  fun extend_trtab name trfuns tab = Symtab.extend (remove_trtab trfuns tab, trfuns)
    6.15 -  handle Symtab.DUPS cs => err_dup_trfuns name cs;
    6.16 +  handle Symtab.DUP c => err_dup_trfun name c;
    6.17  
    6.18  fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
    6.19 -  handle Symtab.DUPS cs => err_dup_trfuns name cs;
    6.20 +  handle Symtab.DUP c => err_dup_trfun name c;
    6.21  
    6.22  
    6.23  (* print (ast) translations *)
     7.1 --- a/src/Pure/Thy/term_style.ML	Sun Jul 08 19:51:55 2007 +0200
     7.2 +++ b/src/Pure/Thy/term_style.ML	Sun Jul 08 19:51:58 2007 +0200
     7.3 @@ -18,8 +18,8 @@
     7.4  
     7.5  (* style data *)
     7.6  
     7.7 -fun err_dup_styles names =
     7.8 -  error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
     7.9 +fun err_dup_style name =
    7.10 +  error ("Duplicate declaration of antiquote style: " ^ quote name);
    7.11  
    7.12  structure StyleData = TheoryDataFun
    7.13  (
    7.14 @@ -28,7 +28,7 @@
    7.15    val copy = I;
    7.16    val extend = I;
    7.17    fun merge _ tabs : T = Symtab.merge (eq_snd (op =)) tabs
    7.18 -    handle Symtab.DUPS dups => err_dup_styles dups;
    7.19 +    handle Symtab.DUP dup => err_dup_style dup;
    7.20  );
    7.21  
    7.22  fun print_styles thy =
    7.23 @@ -44,7 +44,7 @@
    7.24  
    7.25  fun add_style name style thy =
    7.26    StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy
    7.27 -    handle Symtab.DUP _ => err_dup_styles [name];
    7.28 +    handle Symtab.DUP _ => err_dup_style name;
    7.29  
    7.30  
    7.31  (* predefined styles *)
     8.1 --- a/src/Pure/codegen.ML	Sun Jul 08 19:51:55 2007 +0200
     8.2 +++ b/src/Pure/codegen.ML	Sun Jul 08 19:51:58 2007 +0200
     8.3 @@ -894,7 +894,7 @@
     8.4             (map (fn s => case Symtab.lookup graphs s of
     8.5                  NONE => error ("Undefined code module: " ^ s)
     8.6                | SOME gr => gr) modules))
     8.7 -      handle Graph.DUPS ks => error ("Duplicate code for " ^ commas ks);
     8.8 +      handle Graph.DUP k => error ("Duplicate code for " ^ k);
     8.9      fun expand (t as Abs _) = t
    8.10        | expand t = (case fastype_of t of
    8.11            Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t);
     9.1 --- a/src/Pure/consts.ML	Sun Jul 08 19:51:55 2007 +0200
     9.2 +++ b/src/Pure/consts.ML	Sun Jul 08 19:51:58 2007 +0200
     9.3 @@ -196,14 +196,14 @@
     9.4  
     9.5  (** build consts **)
     9.6  
     9.7 -fun err_dup_consts cs =
     9.8 -  error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
     9.9 +fun err_dup_const c =
    9.10 +  error ("Duplicate declaration of constant " ^ quote c);
    9.11  
    9.12 -fun err_inconsistent_constraints cs =
    9.13 -  error ("Inconsistent type constraints for constant(s) " ^ commas_quote cs);
    9.14 +fun err_inconsistent_constraints c =
    9.15 +  error ("Inconsistent type constraints for constant " ^ quote c);
    9.16  
    9.17  fun extend_decls naming decl tab = NameSpace.extend_table naming [decl] tab
    9.18 -  handle Symtab.DUPS cs => err_dup_consts cs;
    9.19 +  handle Symtab.DUP c => err_dup_const c;
    9.20  
    9.21  
    9.22  (* name space *)
    9.23 @@ -303,9 +303,9 @@
    9.24        rev_abbrevs = rev_abbrevs2, do_expand = do_expand2}, _)) =
    9.25    let
    9.26      val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2)
    9.27 -      handle Symtab.DUPS cs => err_dup_consts cs;
    9.28 +      handle Symtab.DUP c => err_dup_const c;
    9.29      val constraints' = Symtab.merge (op =) (constraints1, constraints2)
    9.30 -      handle Symtab.DUPS cs => err_inconsistent_constraints cs;
    9.31 +      handle Symtab.DUP c => err_inconsistent_constraints c;
    9.32      val rev_abbrevs' = (rev_abbrevs1, rev_abbrevs2) |> Symtab.join
    9.33        (K (Library.merge (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u')));
    9.34      val do_expand' = do_expand1 orelse do_expand2;
    10.1 --- a/src/Pure/simplifier.ML	Sun Jul 08 19:51:55 2007 +0200
    10.2 +++ b/src/Pure/simplifier.ML	Sun Jul 08 19:51:58 2007 +0200
    10.3 @@ -167,8 +167,7 @@
    10.4  
    10.5  (** named simprocs **)
    10.6  
    10.7 -fun err_dup_simprocs ds =
    10.8 -  error ("Duplicate simproc(s): " ^ commas_quote ds);
    10.9 +fun err_dup_simproc name = error ("Duplicate simproc: " ^ quote name);
   10.10  
   10.11  
   10.12  (* data *)
   10.13 @@ -179,7 +178,7 @@
   10.14    val empty = NameSpace.empty_table;
   10.15    val extend = I;
   10.16    fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
   10.17 -    handle Symtab.DUPS ds => err_dup_simprocs ds;
   10.18 +    handle Symtab.DUP dup => err_dup_simproc dup;
   10.19  );
   10.20  
   10.21  
   10.22 @@ -229,7 +228,7 @@
   10.23          context
   10.24          |> Simprocs.map (fn simprocs =>
   10.25              NameSpace.extend_table naming [(name', simproc')] simprocs
   10.26 -              handle Symtab.DUPS ds => err_dup_simprocs ds)
   10.27 +              handle Symtab.DUP dup => err_dup_simproc dup)
   10.28          |> map_ss (fn ss => ss addsimprocs [simproc'])
   10.29        end)
   10.30    end;
    11.1 --- a/src/Pure/sorts.ML	Sun Jul 08 19:51:55 2007 +0200
    11.2 +++ b/src/Pure/sorts.ML	Sun Jul 08 19:51:58 2007 +0200
    11.3 @@ -183,8 +183,7 @@
    11.4  
    11.5  (* classes *)
    11.6  
    11.7 -fun err_dup_classes cs =
    11.8 -  error ("Duplicate declaration of class(es): " ^ commas_quote cs);
    11.9 +fun err_dup_class c = error ("Duplicate declaration of class: " ^ quote c);
   11.10  
   11.11  fun err_cyclic_classes pp css =
   11.12    error (cat_lines (map (fn cs =>
   11.13 @@ -193,7 +192,7 @@
   11.14  fun add_class pp (c, cs) = map_classes (fn classes =>
   11.15    let
   11.16      val classes' = classes |> Graph.new_node (c, serial ())
   11.17 -      handle Graph.DUP dup => err_dup_classes [dup];
   11.18 +      handle Graph.DUP dup => err_dup_class dup;
   11.19      val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs)
   11.20        handle Graph.CYCLES css => err_cyclic_classes pp css;
   11.21    in classes'' end);
   11.22 @@ -274,7 +273,7 @@
   11.23      Algebra {classes = classes2, arities = arities2}) =
   11.24    let
   11.25      val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2)
   11.26 -      handle Graph.DUPS cs => err_dup_classes cs
   11.27 +      handle Graph.DUP c => err_dup_class c
   11.28            | Graph.CYCLES css => err_cyclic_classes pp css;
   11.29      val algebra0 = make_algebra (classes', Symtab.empty);
   11.30      val arities' = Symtab.empty
    12.1 --- a/src/Pure/theory.ML	Sun Jul 08 19:51:55 2007 +0200
    12.2 +++ b/src/Pure/theory.ML	Sun Jul 08 19:51:58 2007 +0200
    12.3 @@ -96,8 +96,8 @@
    12.4  fun make_thy (axioms, defs, oracles) =
    12.5    Thy {axioms = axioms, defs = defs, oracles = oracles};
    12.6  
    12.7 -fun err_dup_axms dups = error ("Duplicate axiom(s): " ^ commas_quote dups);
    12.8 -fun err_dup_oras dups = error ("Duplicate oracle(s): " ^ commas_quote dups);
    12.9 +fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
   12.10 +fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
   12.11  
   12.12  structure ThyData = TheoryDataFun
   12.13  (
   12.14 @@ -115,7 +115,7 @@
   12.15        val axioms = NameSpace.empty_table;
   12.16        val defs = Defs.merge pp (defs1, defs2);
   12.17        val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
   12.18 -        handle Symtab.DUPS dups => err_dup_oras dups;
   12.19 +        handle Symtab.DUP dup => err_dup_ora dup;
   12.20      in make_thy (axioms, defs, oracles) end;
   12.21  );
   12.22  
   12.23 @@ -182,7 +182,7 @@
   12.24    let
   12.25      val axms = map (apsnd (Compress.term thy o Logic.varify) o prep_axm thy) raw_axms;
   12.26      val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms
   12.27 -      handle Symtab.DUPS dups => err_dup_axms dups;
   12.28 +      handle Symtab.DUP dup => err_dup_axm dup;
   12.29    in axioms' end);
   12.30  
   12.31  in
   12.32 @@ -307,7 +307,7 @@
   12.33  
   12.34  fun add_oracle (bname, oracle) thy = thy |> map_oracles (fn oracles =>
   12.35    NameSpace.extend_table (Sign.naming_of thy) [(bname, (oracle, stamp ()))] oracles
   12.36 -    handle Symtab.DUPS dups => err_dup_oras dups);
   12.37 +    handle Symtab.DUP dup => err_dup_ora dup);
   12.38  
   12.39  end;
   12.40  
    13.1 --- a/src/Pure/type.ML	Sun Jul 08 19:51:55 2007 +0200
    13.2 +++ b/src/Pure/type.ML	Sun Jul 08 19:51:58 2007 +0200
    13.3 @@ -570,7 +570,7 @@
    13.4  
    13.5  fun merge_types (types1, types2) =
    13.6    NameSpace.merge_tables (Library.eq_snd (op = : serial * serial -> bool)) (types1, types2)
    13.7 -    handle Symtab.DUPS (d :: _) => err_in_decls d (the_decl types1 d) (the_decl types2 d);
    13.8 +    handle Symtab.DUP d => err_in_decls d (the_decl types1 d) (the_decl types2 d);
    13.9  
   13.10  end;
   13.11