diff -r 3ff5a2e05810 -r f9cf9e62d11c src/HOL/Tools/ATP/reduce_axiomsN.ML
--- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Oct 04 14:14:33 2006 +0200
+++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Oct 04 14:17:38 2006 +0200
@@ -65,7 +65,7 @@
 (*Add a const/type pair to the table, but a [] entry means a standard connective,
   which we ignore.*)
 fun add_const_typ_table ((c,ctyps), tab) =
-  Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => ctyps ins ctyps_list) 
+  Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => insert (op =) ctyps ctyps_list) 
     tab;
 
 (*Free variables are included, as well as constants, to handle locales*)