src/Pure/simplifier.ML
changeset 23655 d2d1138e0ddc
parent 23598 e03a43b8178c
child 24024 c46bd50df3f9
     1.1 --- a/src/Pure/simplifier.ML	Sun Jul 08 19:51:55 2007 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Sun Jul 08 19:51:58 2007 +0200
     1.3 @@ -167,8 +167,7 @@
     1.4  
     1.5  (** named simprocs **)
     1.6  
     1.7 -fun err_dup_simprocs ds =
     1.8 -  error ("Duplicate simproc(s): " ^ commas_quote ds);
     1.9 +fun err_dup_simproc name = error ("Duplicate simproc: " ^ quote name);
    1.10  
    1.11  
    1.12  (* data *)
    1.13 @@ -179,7 +178,7 @@
    1.14    val empty = NameSpace.empty_table;
    1.15    val extend = I;
    1.16    fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
    1.17 -    handle Symtab.DUPS ds => err_dup_simprocs ds;
    1.18 +    handle Symtab.DUP dup => err_dup_simproc dup;
    1.19  );
    1.20  
    1.21  
    1.22 @@ -229,7 +228,7 @@
    1.23          context
    1.24          |> Simprocs.map (fn simprocs =>
    1.25              NameSpace.extend_table naming [(name', simproc')] simprocs
    1.26 -              handle Symtab.DUPS ds => err_dup_simprocs ds)
    1.27 +              handle Symtab.DUP dup => err_dup_simproc dup)
    1.28          |> map_ss (fn ss => ss addsimprocs [simproc'])
    1.29        end)
    1.30    end;