--- 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"};