--- 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