diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/Import/HOL_Light_Maps.thy
--- a/src/HOL/Import/HOL_Light_Maps.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -198,7 +198,7 @@
   by simp
 
 import_const_map MOD : mod
-import_const_map DIV : div
+import_const_map DIV : divide
 
 lemma DIVISION_0:
   "\<forall>m n\<Colon>nat. if n = id 0 then m div n = id 0 \<and> m mod n = m else m = m div n * n + m mod n \<and> m mod n < n"