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