changeset 35983 | 27e2fa7d4ce7 |
parent 35408 | b48ab741683b |
child 36349 | 39be26d1bc28 |
--- a/src/HOL/Tools/numeral_simprocs.ML Sat Mar 27 00:08:39 2010 +0100 +++ b/src/HOL/Tools/numeral_simprocs.ML Sat Mar 27 02:10:00 2010 +0100 @@ -344,8 +344,7 @@ 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; + val is_numeral = can HOLogic.dest_number end; structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);