# HG changeset patch
# User webertj
# Date 1156457410 -7200
# Node ID 5a6e152a71144a9384d6e6043e5f80350239ee77
# Parent  40757f475eb0aca50c4e344abf9303f6a9311306
avoid duplicate tactics

diff -r 40757f475eb0 -r 5a6e152a7114 src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Thu Aug 24 23:51:46 2006 +0200
+++ b/src/HOL/Integ/presburger.ML	Fri Aug 25 00:10:10 2006 +0200
@@ -363,13 +363,15 @@
 fun presburger_method q a i = Method.METHOD (fn facts =>
   Method.insert_tac facts 1 THEN presburger_tac q a i)
 
+val presburger_arith_tac = mk_arith_tactic "presburger" (fn i => fn st =>
+  (warning "Trying full Presburger arithmetic ...";
+   presburger_tac true true i st));
+
 val setup =
   Method.add_method ("presburger",
     presburger_args presburger_method,
     "decision procedure for Presburger arithmetic") #>
-  arith_tactic_add (mk_arith_tactic "presburger" (fn i => fn st =>
-    (warning "Trying full Presburger arithmetic ...";
-     presburger_tac true true i st)));
+  arith_tactic_add presburger_arith_tac;
 
 end;
 
diff -r 40757f475eb0 -r 5a6e152a7114 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Thu Aug 24 23:51:46 2006 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Fri Aug 25 00:10:10 2006 +0200
@@ -363,13 +363,15 @@
 fun presburger_method q a i = Method.METHOD (fn facts =>
   Method.insert_tac facts 1 THEN presburger_tac q a i)
 
+val presburger_arith_tac = mk_arith_tactic "presburger" (fn i => fn st =>
+  (warning "Trying full Presburger arithmetic ...";
+   presburger_tac true true i st));
+
 val setup =
   Method.add_method ("presburger",
     presburger_args presburger_method,
     "decision procedure for Presburger arithmetic") #>
-  arith_tactic_add (mk_arith_tactic "presburger" (fn i => fn st =>
-    (warning "Trying full Presburger arithmetic ...";
-     presburger_tac true true i st)));
+  arith_tactic_add presburger_arith_tac;
 
 end;
 
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 =