# HG changeset patch
# User wenzelm
# Date 1288776037 -3600
# Node ID 54e8be8b4de05a53f62aa8234fcbd90e8ae3818e
# Parent  dff9f73a376339797bb297ffc2d7bdc125dfd6b0
eliminated dead code;

diff -r dff9f73a3763 -r 54e8be8b4de0 src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Wed Nov 03 10:18:05 2010 +0100
+++ b/src/ZF/int_arith.ML	Wed Nov 03 10:20:37 2010 +0100
@@ -64,8 +64,6 @@
 fun long_mk_sum []        = zero
   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
 
-val dest_plus = FOLogic.dest_bin @{const_name "zadd"} @{typ i};
-
 (*decompose additions AND subtractions as a sum*)
 fun dest_summing (pos, Const (@{const_name "zadd"}, _) $ t $ u, ts) =
         dest_summing (pos, t, dest_summing (pos, u, ts))
@@ -76,9 +74,6 @@
 
 fun dest_sum t = dest_summing (true, t, []);
 
-val mk_diff = FOLogic.mk_binop @{const_name "zdiff"};
-val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} @{typ i};
-
 val one = mk_numeral 1;
 val mk_times = FOLogic.mk_binop @{const_name "zmult"};