# HG changeset patch
# User haftmann
# Date 1347732805 -7200
# Node ID 1677084562698abb87d3a47aa1ce976a67122db6
# Parent  ac2e29fc57a5605081abc2776d8b7ab049aa31f7
dropped some unused identifiers

diff -r ac2e29fc57a5 -r 167708456269 src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Sat Sep 15 16:09:53 2012 +0200
+++ b/src/HOL/Tools/arith_data.ML	Sat Sep 15 20:13:25 2012 +0200
@@ -51,7 +51,7 @@
 fun gen_arith_tac verbose ctxt =
   let
     val tactics = Arith_Tactics.get (Proof_Context.theory_of ctxt);
-    fun invoke (_, (name, tac)) k st = tac verbose ctxt k st;
+    fun invoke (_, (_, tac)) k st = tac verbose ctxt k st;
   in FIRST' (map invoke (rev tactics)) end;
 
 val arith_tac = gen_arith_tac false;
diff -r ac2e29fc57a5 -r 167708456269 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Sat Sep 15 16:09:53 2012 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sat Sep 15 20:13:25 2012 +0200
@@ -342,7 +342,7 @@
 (* If they're both inequalities, 1st coefficient must be +ve, 2nd -ve.       *)
 (* ------------------------------------------------------------------------- *)
 
-fun elim_var v (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) =
+fun elim_var v (i1 as Lineq(_,ty1,l1,_)) (i2 as Lineq(_,ty2,l2,_)) =
   let val c1 = nth l1 v and c2 = nth l2 v
       val m = Integer.lcm (abs c1) (abs c2)
       val m1 = m div (abs c1) and m2 = m div (abs c2)
@@ -879,7 +879,7 @@
 let val {neqE, ...} = get_data ctxt
     fun elim_neq [] (asms', []) = Tip (rev asms')
       | elim_neq [] (asms', asms) = Tip (rev asms' @ asms)
-      | elim_neq (neq :: neqs) (asms', []) = elim_neq neqs ([],rev asms')
+      | elim_neq (_ :: neqs) (asms', []) = elim_neq neqs ([],rev asms')
       | elim_neq (neqs as (neq :: _)) (asms', asm::asms) =
       (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) [neq] of
         SOME spl =>