1.1 --- a/src/Pure/simplifier.ML	Sat Oct 24 19:04:57 2009 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Sat Oct 24 19:20:03 2009 +0200
     1.3 @@ -143,9 +143,6 @@
     1.4  
     1.5  (** named simprocs **)
     1.6  
     1.7 -fun err_dup_simproc name = error ("Duplicate simproc: " ^ quote name);
     1.8 -
     1.9 -
    1.10  (* data *)
    1.11  
    1.12  structure Simprocs = GenericDataFun
    1.13 @@ -153,8 +150,7 @@
    1.14    type T = simproc NameSpace.table;
    1.15    val empty = NameSpace.empty_table;
    1.16    val extend = I;
    1.17 -  fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
    1.18 -    handle Symtab.DUP dup => err_dup_simproc dup;
    1.19 +  fun merge _ simprocs = NameSpace.merge_tables simprocs;
    1.20  );
    1.21  
    1.22  
    1.23 @@ -201,9 +197,7 @@
    1.24          val b' = Morphism.binding phi b;
    1.25          val simproc' = morph_simproc phi simproc;
    1.26        in
    1.27 -        Simprocs.map (fn simprocs =>
    1.28 -          NameSpace.define naming (b', simproc') simprocs |> snd
    1.29 -            handle Symtab.DUP dup => err_dup_simproc dup)
    1.30 +        Simprocs.map (#2 o NameSpace.define true naming (b', simproc'))
    1.31          #> map_ss (fn ss => ss addsimprocs [simproc'])
    1.32        end)
    1.33    end;