# HG changeset patch
# User huffman
# Date 1238092430 25200
# Node ID afca5be252d62607b8352041efe5d0427e6396bd
# Parent  da8598ec4e9810693ea1ffe894ff6cba51c66db1
parameterize assoc_fold with is_numeral predicate

diff -r da8598ec4e98 -r afca5be252d6 src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Thu Mar 26 14:30:20 2009 +0000
+++ b/src/HOL/Tools/int_arith.ML	Thu Mar 26 11:33:50 2009 -0700
@@ -377,6 +377,8 @@
 struct
   val assoc_ss = HOL_ss addsimps @{thms mult_ac}
   val eq_reflection = eq_reflection
+  fun is_numeral (Const(@{const_name Int.number_of}, _) $ _) = true
+    | is_numeral _ = false;
 end;
 
 structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
diff -r da8598ec4e98 -r afca5be252d6 src/Provers/Arith/assoc_fold.ML
--- a/src/Provers/Arith/assoc_fold.ML	Thu Mar 26 14:30:20 2009 +0000
+++ b/src/Provers/Arith/assoc_fold.ML	Thu Mar 26 11:33:50 2009 -0700
@@ -12,6 +12,7 @@
 sig
   val assoc_ss: simpset
   val eq_reflection: thm
+  val is_numeral: term -> bool
 end;
 
 signature ASSOC_FOLD =
@@ -29,10 +30,9 @@
 
 (*Separate the literals from the other terms being combined*)
 fun sift_terms plus (t, (lits,others)) =
+  if Data.is_numeral t then (t::lits, others) (*new literal*) else
   (case t of
-    Const (@{const_name Int.number_of}, _) $ _ =>       (* FIXME logic dependent *)
-      (t::lits, others)         (*new literal*)
-  | (f as Const _) $ x $ y =>
+    (f as Const _) $ x $ y =>
       if f = plus
       then sift_terms plus (x, sift_terms plus (y, (lits,others)))
       else (lits, t::others)    (*arbitrary summand*)