src/HOL/Tools/numeral_simprocs.ML
changeset 35983 27e2fa7d4ce7
parent 35408 b48ab741683b
child 36349 39be26d1bc28
     1.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Sat Mar 27 00:08:39 2010 +0100
     1.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Mar 27 02:10:00 2010 +0100
     1.3 @@ -344,8 +344,7 @@
     1.4  struct
     1.5    val assoc_ss = HOL_ss addsimps @{thms mult_ac}
     1.6    val eq_reflection = eq_reflection
     1.7 -  fun is_numeral (Const(@{const_name Int.number_of}, _) $ _) = true
     1.8 -    | is_numeral _ = false;
     1.9 +  val is_numeral = can HOLogic.dest_number
    1.10  end;
    1.11  
    1.12  structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);