src/HOL/Tools/nat_numeral_simprocs.ML
changeset 37388 793618618f78
parent 35408 b48ab741683b
child 38864 4abe644fcea5
     1.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Tue Jun 08 16:37:19 2010 +0200
     1.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Tue Jun 08 16:37:22 2010 +0200
     1.3 @@ -97,7 +97,7 @@
     1.4  
     1.5  (*Split up a sum into the list of its constituent terms, on the way removing any
     1.6    Sucs and counting them.*)
     1.7 -fun dest_Suc_sum (Const ("Suc", _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
     1.8 +fun dest_Suc_sum (Const (@{const_name Suc}, _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
     1.9    | dest_Suc_sum (t, (k,ts)) = 
    1.10        let val (t1,t2) = dest_plus t
    1.11        in  dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts)))  end