diff -r 40757f475eb0 -r 5a6e152a7114 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Thu Aug 24 23:51:46 2006 +0200
+++ b/src/HOL/arith_data.ML	Fri Aug 25 00:10:10 2006 +0200
@@ -209,6 +209,8 @@
 
 fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2);
 
+val merge_arith_tactics = gen_merge_lists eq_arith_tactic;
+
 structure ArithTheoryData = TheoryDataFun
 (struct
   val name = "HOL/arith";
@@ -224,7 +226,7 @@
    {splits = Drule.merge_rules (splits1, splits2),
     inj_consts = merge_lists inj_consts1 inj_consts2,
     discrete = merge_lists discrete1 discrete2,
-    tactics = gen_merge_lists eq_arith_tactic tactics1 tactics2};
+    tactics = merge_arith_tactics tactics1 tactics2};
   fun print _ _ = ();
 end);
 
@@ -239,7 +241,7 @@
   {splits = splits, inj_consts = c :: inj_consts, discrete = discrete, tactics= tactics});
 
 fun arith_tactic_add tac = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
-  {splits= splits, inj_consts= inj_consts, discrete= discrete, tactics= tactics @ [tac]});
+  {splits= splits, inj_consts= inj_consts, discrete= discrete, tactics= merge_arith_tactics tactics [tac]});
 
 
 signature HOL_LIN_ARITH_DATA =