--- a/src/HOL/Library/Saturated.thy Sat Apr 11 16:19:14 2015 +0100
+++ b/src/HOL/Library/Saturated.thy Sat Apr 11 16:19:59 2015 +0100
@@ -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
--- a/src/HOL/Library/Stream.thy Sat Apr 11 16:19:14 2015 +0100
+++ b/src/HOL/Library/Stream.thy Sat Apr 11 16:19:59 2015 +0100
@@ -18,14 +18,17 @@
map: smap
rel: stream_all2
+context
+begin
+
(*for code generation only*)
-definition smember :: "'a \<Rightarrow> 'a stream \<Rightarrow> bool" where
+qualified definition smember :: "'a \<Rightarrow> 'a stream \<Rightarrow> bool" where
[code_abbrev]: "smember x s \<longleftrightarrow> x \<in> sset s"
lemma smember_code[code, simp]: "smember x (y ## s) = (if x = y then True else smember x s)"
unfolding smember_def by auto
-hide_const (open) smember
+end
lemmas smap_simps[simp] = stream.map_sel
lemmas shd_sset = stream.set_sel(1)