# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1428765599 -3600
# Node ID 4dda564e8a5ddcbc35ae45758b770c2b8f0abcce
# Parent  05d4dce039c64fe701d7d49f58b5aa65e648a31e# Parent  3eef7a43cd51ff1e77ab57c071f86f901e33149c
Merge

diff -r 05d4dce039c6 -r 4dda564e8a5d src/HOL/Library/Saturated.thy
--- 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
 
diff -r 05d4dce039c6 -r 4dda564e8a5d src/HOL/Library/Stream.thy
--- 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)