diff -r dcfc28144858 -r 3a4400985780 src/HOL/Library/Discrete.thy
--- a/src/HOL/Library/Discrete.thy	Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/Discrete.thy	Fri Sep 04 19:22:13 2015 +0200
@@ -8,7 +8,10 @@
 
 subsection \<open>Discrete logarithm\<close>
 
-fun log :: "nat \<Rightarrow> nat"
+context
+begin
+
+qualified fun log :: "nat \<Rightarrow> nat"
   where [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))"
 
 lemma log_zero [simp]: "log 0 = 0"
@@ -67,7 +70,7 @@
 
 subsection \<open>Discrete square root\<close>
 
-definition sqrt :: "nat \<Rightarrow> nat"
+qualified definition sqrt :: "nat \<Rightarrow> nat"
   where "sqrt n = Max {m. m\<^sup>2 \<le> n}"
 
 lemma sqrt_aux:
@@ -173,7 +176,6 @@
 lemma sqrt_le: "sqrt n \<le> n"
   using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)
 
-hide_const (open) log sqrt
-
 end
 
+end
\ No newline at end of file