# HG changeset patch
# User wenzelm
# Date 1428750777 -7200
# Node ID 3eef7a43cd51ff1e77ab57c071f86f901e33149c
# Parent  5fe58ca9cf40e0dd4f98864281e9cd813b77dbbf
tuned;

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
 
diff -r 5fe58ca9cf40 -r 3eef7a43cd51 src/HOL/Library/Stream.thy
--- a/src/HOL/Library/Stream.thy	Sat Apr 11 12:47:46 2015 +0200
+++ b/src/HOL/Library/Stream.thy	Sat Apr 11 13:12:57 2015 +0200
@@ -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)