diff -r 30a0f5879d90 -r 46a0bb3d3a7b src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Thu Sep 16 18:59:59 2021 +0200
+++ b/src/ZF/arith_data.ML	Sun Sep 19 20:47:16 2021 +0200
@@ -36,12 +36,6 @@
   | mk_sum [t,u]     = mk_plus (t, u)
   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
 
-(*this version ALWAYS includes a trailing zero*)
-fun long_mk_sum []        = zero
-  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-
-val dest_plus = FOLogic.dest_bin \<^const_name>\<open>Arith.add\<close> iT;
-
 (* dest_sum *)
 
 fun dest_sum \<^Const_>\<open>zero\<close> = []
@@ -63,8 +57,6 @@
 fun is_eq_thm th =
     can FOLogic.dest_eq (FOLogic.dest_Trueprop (Thm.prop_of th));
 
-fun add_chyps chyps ct = Drule.list_implies (map Thm.cprop_of chyps, ct);
-
 fun prove_conv name tacs ctxt prems (t,u) =
   if t aconv u then NONE
   else