# HG changeset patch
# User huffman
# Date 1343410041 -7200
# Node ID 12aa0cb2b4470708cd874c17a13a3e4ec1a0f89f
# Parent  e0875d956a6b3ec4834fc9213871244de5d0acea
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used

diff -r e0875d956a6b -r 12aa0cb2b447 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Jul 27 17:59:18 2012 +0200
+++ b/src/HOL/Divides.thy	Fri Jul 27 19:27:21 2012 +0200
@@ -693,8 +693,20 @@
   val div_name = @{const_name div};
   val mod_name = @{const_name mod};
   val mk_binop = HOLogic.mk_binop;
-  val mk_sum = Nat_Arith.mk_sum;
-  val dest_sum = Nat_Arith.dest_sum;
+  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
+  val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
+  fun mk_sum [] = HOLogic.zero
+    | mk_sum [t] = t
+    | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+  fun dest_sum tm =
+    if HOLogic.is_zero tm then []
+    else
+      (case try HOLogic.dest_Suc tm of
+        SOME t => HOLogic.Suc_zero :: dest_sum t
+      | NONE =>
+          (case try dest_plus tm of
+            SOME (t, u) => dest_sum t @ dest_sum u
+          | NONE => [tm]));
 
   val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
 
diff -r e0875d956a6b -r 12aa0cb2b447 src/HOL/Tools/nat_arith.ML
--- a/src/HOL/Tools/nat_arith.ML	Fri Jul 27 17:59:18 2012 +0200
+++ b/src/HOL/Tools/nat_arith.ML	Fri Jul 27 19:27:21 2012 +0200
@@ -10,40 +10,11 @@
   val cancel_eq_conv: conv
   val cancel_le_conv: conv
   val cancel_less_conv: conv
-  (* legacy functions: *)
-  val mk_sum: term list -> term
-  val mk_norm_sum: term list -> term
-  val dest_sum: term -> term list
 end;
 
 structure Nat_Arith: NAT_ARITH =
 struct
 
-(** abstract syntax of structure nat: 0, Suc, + **)
-
-val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
-val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
-
-fun mk_sum [] = HOLogic.zero
-  | mk_sum [t] = t
-  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-
-(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
-fun mk_norm_sum ts =
-  let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
-    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
-  end;
-
-fun dest_sum tm =
-  if HOLogic.is_zero tm then []
-  else
-    (case try HOLogic.dest_Suc tm of
-      SOME t => HOLogic.Suc_zero :: dest_sum t
-    | NONE =>
-        (case try dest_plus tm of
-          SOME (t, u) => dest_sum t @ dest_sum u
-        | NONE => [tm]));
-
 val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
       by (simp only: add_ac)}
 val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"