src/HOL/Tools/Nitpick/nitpick_preproc.ML
changeset 60352 d46de31a50c4
parent 59582 0fbed69ff081
child 61324 d4ec7594f558
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Jun 01 18:59:21 2015 +0200
@@ -56,7 +56,7 @@
   let
     fun aux (t1 $ t2) = aux t1 orelse aux t2
       | aux (Const (s, T)) =
-        ((s = @{const_name times} orelse s = @{const_name div}) andalso
+        ((s = @{const_name times} orelse s = @{const_name Rings.divide}) andalso
          is_integer_type (body_type T)) orelse
         (String.isPrefix numeral_prefix s andalso
          let val n = the (Int.fromString (unprefix numeral_prefix s)) in