diff -r 5fe58ca9cf40 -r 3eef7a43cd51 src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Sat Apr 11 12:47:46 2015 +0200
+++ b/src/HOL/Library/Saturated.thy	Sat Apr 11 13:12:57 2015 +0200
@@ -161,13 +161,18 @@
   "of_nat (numeral k) = (numeral k :: 'a::len sat)"
   by simp
 
-definition sat_of_nat :: "nat \<Rightarrow> ('a::len) sat"
+context
+begin
+
+qualified definition sat_of_nat :: "nat \<Rightarrow> ('a::len) sat"
   where [code_abbrev]: "sat_of_nat = of_nat"
 
 lemma [code abstract]:
   "nat_of (sat_of_nat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
   by (simp add: sat_of_nat_def)
 
+end
+
 instance sat :: (len) finite
 proof
   show "finite (UNIV::'a sat set)"
@@ -271,7 +276,5 @@
     by (auto simp: bot_sat_def)
 qed
 
-hide_const (open) sat_of_nat
-
 end