1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Jan 27 12:24:00 2011 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Jan 26 20:51:09 2011 +0100
     1.3 @@ -287,7 +287,7 @@
     1.4        | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop @{const_name sdiv}
     1.5            (fst (tm_of vs e), fst (tm_of vs e')), integerN)
     1.6  
     1.7 -      | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name smod}
     1.8 +      | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name mod}
     1.9            (fst (tm_of vs e), fst (tm_of vs e')), integerN)
    1.10  
    1.11        | tm_of vs (Funct ("-", [e])) =