# HG changeset patch
# User wenzelm
# Date 1441387333 -7200
# Node ID 3a44009857801a5a7e907170cdbe24176252be9f
# Parent  dcfc2814485821d5d74ef685e71c7347fe9f1453
modernized name space management -- more uniform qualification;

diff -r dcfc28144858 -r 3a4400985780 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/Cardinality.thy	Fri Sep 04 19:22:13 2015 +0200
@@ -410,7 +410,10 @@
   possibly slow dictionary constructions.
 \<close>
 
-definition card_UNIV' :: "'a card_UNIV"
+context
+begin
+
+qualified definition card_UNIV' :: "'a card_UNIV"
 where [code del]: "card_UNIV' = Phantom('a) CARD('a)"
 
 lemma CARD_code [code_unfold]:
@@ -421,7 +424,7 @@
   "card_UNIV' = card_UNIV"
 by(simp add: card_UNIV card_UNIV'_def)
 
-hide_const (open) card_UNIV'
+end
 
 lemma card_Compl:
   "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
@@ -430,7 +433,7 @@
 context fixes xs :: "'a :: finite_UNIV list"
 begin
 
-definition finite' :: "'a set \<Rightarrow> bool"
+qualified definition finite' :: "'a set \<Rightarrow> bool"
 where [simp, code del, code_abbrev]: "finite' = finite"
 
 lemma finite'_code [code]:
@@ -443,7 +446,7 @@
 context fixes xs :: "'a :: card_UNIV list"
 begin
 
-definition card' :: "'a set \<Rightarrow> nat" 
+qualified definition card' :: "'a set \<Rightarrow> nat" 
 where [simp, code del, code_abbrev]: "card' = card"
  
 lemma card'_code [code]:
@@ -452,7 +455,7 @@
 by(simp_all add: List.card_set card_Compl card_UNIV)
 
 
-definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+qualified definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
 where [simp, code del, code_abbrev]: "subset' = op \<subseteq>"
 
 lemma subset'_code [code]:
@@ -462,7 +465,7 @@
 by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card])
   (metis finite_compl finite_set rev_finite_subset)
 
-definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+qualified definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
 where [simp, code del, code_abbrev]: "eq_set = op ="
 
 lemma eq_set_code [code]:
@@ -538,7 +541,4 @@
   by eval
 end
 
-hide_const (open) card' finite' subset' eq_set
-
 end
-
diff -r dcfc28144858 -r 3a4400985780 src/HOL/Library/Code_Binary_Nat.thy
--- a/src/HOL/Library/Code_Binary_Nat.thy	Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/Code_Binary_Nat.thy	Fri Sep 04 19:22:13 2015 +0200
@@ -40,6 +40,9 @@
 
 subsection \<open>Basic arithmetic\<close>
 
+context
+begin
+
 lemma [code, code del]:
   "(plus :: nat \<Rightarrow> _) = plus" ..
 
@@ -51,7 +54,7 @@
 
 text \<open>Bounded subtraction needs some auxiliary\<close>
 
-definition dup :: "nat \<Rightarrow> nat" where
+qualified definition dup :: "nat \<Rightarrow> nat" where
   "dup n = n + n"
 
 lemma dup_code [code]:
@@ -59,7 +62,7 @@
   "dup (nat_of_num k) = nat_of_num (Num.Bit0 k)"
   by (simp_all add: dup_def numeral_Bit0)
 
-definition sub :: "num \<Rightarrow> num \<Rightarrow> nat option" where
+qualified definition sub :: "num \<Rightarrow> num \<Rightarrow> nat option" where
   "sub k l = (if k \<ge> l then Some (numeral k - numeral l) else None)"
 
 lemma sub_code [code]:
@@ -139,6 +142,8 @@
   "divmod_nat 0 n = (0, 0)"
   by (simp_all add: prod_eq_iff nat_of_num_numeral)
 
+end
+
 
 subsection \<open>Conversions\<close>
 
@@ -155,7 +160,4 @@
   code_module Code_Binary_Nat \<rightharpoonup>
     (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
-hide_const (open) dup sub
-
 end
-
diff -r dcfc28144858 -r 3a4400985780 src/HOL/Library/Code_Real_Approx_By_Float.thy
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Fri Sep 04 19:22:13 2015 +0200
@@ -85,20 +85,23 @@
     and (OCaml) "Pervasives.sqrt"
 declare sqrt_def[code del]
 
-definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
+context
+begin
+
+qualified definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
 
 lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
   unfolding real_exp_def ..
 
+end
+
 code_printing
-  constant real_exp \<rightharpoonup>
+  constant Code_Real_Approx_By_Float.real_exp \<rightharpoonup>
     (SML) "Math.exp"
     and (OCaml) "Pervasives.exp"
-declare real_exp_def[code del]
+declare Code_Real_Approx_By_Float.real_exp_def[code del]
 declare exp_def[code del]
 
-hide_const (open) real_exp
-
 code_printing
   constant ln \<rightharpoonup>
     (SML) "Math.ln"
@@ -149,7 +152,10 @@
     (SML) "Real.fromInt"
     and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
 
-definition real_of_int :: "int \<Rightarrow> real" where
+context
+begin
+
+qualified definition real_of_int :: "int \<Rightarrow> real" where
   [code_abbrev]: "real_of_int = of_int"
 
 lemma [code]:
@@ -172,7 +178,7 @@
   "- numeral k \<equiv> (of_rat (- numeral k) :: real)"
   by simp
 
-hide_const (open) real_of_int
+end
 
 code_printing
   constant Ratreal \<rightharpoonup> (SML)
diff -r dcfc28144858 -r 3a4400985780 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/Countable.thy	Fri Sep 04 19:22:13 2015 +0200
@@ -66,15 +66,17 @@
 
 subsection \<open>Automatically proving countability of old-style datatypes\<close>
 
-inductive finite_item :: "'a Old_Datatype.item \<Rightarrow> bool" where
+context
+begin
+
+qualified inductive finite_item :: "'a Old_Datatype.item \<Rightarrow> bool" where
   undefined: "finite_item undefined"
 | In0: "finite_item x \<Longrightarrow> finite_item (Old_Datatype.In0 x)"
 | In1: "finite_item x \<Longrightarrow> finite_item (Old_Datatype.In1 x)"
 | Leaf: "finite_item (Old_Datatype.Leaf a)"
 | Scons: "\<lbrakk>finite_item x; finite_item y\<rbrakk> \<Longrightarrow> finite_item (Old_Datatype.Scons x y)"
 
-function
-  nth_item :: "nat \<Rightarrow> ('a::countable) Old_Datatype.item"
+qualified function nth_item :: "nat \<Rightarrow> ('a::countable) Old_Datatype.item"
 where
   "nth_item 0 = undefined"
 | "nth_item (Suc n) =
@@ -97,7 +99,7 @@
 lemma le_sum_encode_Inr: "x \<le> y \<Longrightarrow> x \<le> sum_encode (Inr y)"
 unfolding sum_encode_def by simp
 
-termination
+qualified termination
 by (relation "measure id")
   (auto simp add: sum_encode_eq [symmetric] prod_encode_eq [symmetric]
     le_imp_less_Suc le_sum_encode_Inl le_sum_encode_Inr
@@ -193,7 +195,7 @@
       end)
 \<close>
 
-hide_const (open) finite_item nth_item
+end
 
 
 subsection \<open>Automatically proving countability of datatypes\<close>
diff -r dcfc28144858 -r 3a4400985780 src/HOL/Library/DAList_Multiset.thy
--- a/src/HOL/Library/DAList_Multiset.thy	Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy	Fri Sep 04 19:22:13 2015 +0200
@@ -275,10 +275,13 @@
   "fold_impl fn e ((a,n) # ms) = (fold_impl fn ((fn a n) e) ms)"
 | "fold_impl fn e [] = e"
 
-definition fold :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a, nat) alist \<Rightarrow> 'b"
+context
+begin
+
+qualified definition fold :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a, nat) alist \<Rightarrow> 'b"
   where "fold f e al = fold_impl f e (DAList.impl_of al)"
 
-hide_const (open) fold
+end
 
 context comp_fun_commute
 begin
@@ -348,7 +351,10 @@
 
 end
 
-lift_definition single_alist_entry :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) alist" is "\<lambda>a b. [(a, b)]"
+context
+begin
+
+private lift_definition single_alist_entry :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) alist" is "\<lambda>a b. [(a, b)]"
   by auto
 
 lemma image_mset_Bag [code]:
@@ -368,7 +374,7 @@
   qed
 qed
 
-hide_const single_alist_entry
+end
 
 (* we cannot use (\<lambda>a n. op + (a * n)) for folding, since * is not defined
    in comm_monoid_add *)
diff -r dcfc28144858 -r 3a4400985780 src/HOL/Library/Debug.thy
--- a/src/HOL/Library/Debug.thy	Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/Debug.thy	Fri Sep 04 19:22:13 2015 +0200
@@ -6,37 +6,40 @@
 imports Main
 begin
 
-definition trace :: "String.literal \<Rightarrow> unit" where
+context
+begin
+
+qualified definition trace :: "String.literal \<Rightarrow> unit" where
   [simp]: "trace s = ()"
 
-definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
+qualified definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
   [simp]: "tracing s = id"
 
 lemma [code]:
   "tracing s = (let u = trace s in id)"
   by simp
 
-definition flush :: "'a \<Rightarrow> unit" where
+qualified definition flush :: "'a \<Rightarrow> unit" where
   [simp]: "flush x = ()"
 
-definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where
+qualified definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where
   [simp]: "flushing x = id"
 
 lemma [code, code_unfold]:
   "flushing x = (let u = flush x in id)"
   by simp
 
-definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
+qualified definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
   [simp]: "timing s f x = f x"
 
+end
+
 code_printing
-  constant trace \<rightharpoonup> (Eval) "Output.tracing"
-| constant flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- \<open>note indirection via antiquotation\<close>
-| constant timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
+  constant Debug.trace \<rightharpoonup> (Eval) "Output.tracing"
+| constant Debug.flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- \<open>note indirection via antiquotation\<close>
+| constant Debug.timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
 
 code_reserved Eval Output Timing
 
-hide_const (open) trace tracing flush flushing timing
-
 end
 
diff -r dcfc28144858 -r 3a4400985780 src/HOL/Library/Discrete.thy
--- a/src/HOL/Library/Discrete.thy	Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/Discrete.thy	Fri Sep 04 19:22:13 2015 +0200
@@ -8,7 +8,10 @@
 
 subsection \<open>Discrete logarithm\<close>
 
-fun log :: "nat \<Rightarrow> nat"
+context
+begin
+
+qualified fun log :: "nat \<Rightarrow> nat"
   where [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))"
 
 lemma log_zero [simp]: "log 0 = 0"
@@ -67,7 +70,7 @@
 
 subsection \<open>Discrete square root\<close>
 
-definition sqrt :: "nat \<Rightarrow> nat"
+qualified definition sqrt :: "nat \<Rightarrow> nat"
   where "sqrt n = Max {m. m\<^sup>2 \<le> n}"
 
 lemma sqrt_aux:
@@ -173,7 +176,6 @@
 lemma sqrt_le: "sqrt n \<le> n"
   using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)
 
-hide_const (open) log sqrt
-
 end
 
+end
\ No newline at end of file
diff -r dcfc28144858 -r 3a4400985780 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/Dlist.thy	Fri Sep 04 19:22:13 2015 +0200
@@ -46,61 +46,71 @@
 
 text \<open>Fundamental operations:\<close>
 
-definition empty :: "'a dlist" where
+context
+begin
+
+qualified definition empty :: "'a dlist" where
   "empty = Dlist []"
 
-definition insert :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+qualified definition insert :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
   "insert x dxs = Dlist (List.insert x (list_of_dlist dxs))"
 
-definition remove :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+qualified definition remove :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
   "remove x dxs = Dlist (remove1 x (list_of_dlist dxs))"
 
-definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist" where
+qualified definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist" where
   "map f dxs = Dlist (remdups (List.map f (list_of_dlist dxs)))"
 
-definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+qualified definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
   "filter P dxs = Dlist (List.filter P (list_of_dlist dxs))"
 
+end
+
 
 text \<open>Derived operations:\<close>
 
-definition null :: "'a dlist \<Rightarrow> bool" where
+context
+begin
+
+qualified definition null :: "'a dlist \<Rightarrow> bool" where
   "null dxs = List.null (list_of_dlist dxs)"
 
-definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" where
+qualified definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" where
   "member dxs = List.member (list_of_dlist dxs)"
 
-definition length :: "'a dlist \<Rightarrow> nat" where
+qualified definition length :: "'a dlist \<Rightarrow> nat" where
   "length dxs = List.length (list_of_dlist dxs)"
 
-definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
+qualified definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
   "fold f dxs = List.fold f (list_of_dlist dxs)"
 
-definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
+qualified definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
   "foldr f dxs = List.foldr f (list_of_dlist dxs)"
 
+end
+
 
 subsection \<open>Executable version obeying invariant\<close>
 
 lemma list_of_dlist_empty [simp, code abstract]:
-  "list_of_dlist empty = []"
-  by (simp add: empty_def)
+  "list_of_dlist Dlist.empty = []"
+  by (simp add: Dlist.empty_def)
 
 lemma list_of_dlist_insert [simp, code abstract]:
-  "list_of_dlist (insert x dxs) = List.insert x (list_of_dlist dxs)"
-  by (simp add: insert_def)
+  "list_of_dlist (Dlist.insert x dxs) = List.insert x (list_of_dlist dxs)"
+  by (simp add: Dlist.insert_def)
 
 lemma list_of_dlist_remove [simp, code abstract]:
-  "list_of_dlist (remove x dxs) = remove1 x (list_of_dlist dxs)"
-  by (simp add: remove_def)
+  "list_of_dlist (Dlist.remove x dxs) = remove1 x (list_of_dlist dxs)"
+  by (simp add: Dlist.remove_def)
 
 lemma list_of_dlist_map [simp, code abstract]:
-  "list_of_dlist (map f dxs) = remdups (List.map f (list_of_dlist dxs))"
-  by (simp add: map_def)
+  "list_of_dlist (Dlist.map f dxs) = remdups (List.map f (list_of_dlist dxs))"
+  by (simp add: Dlist.map_def)
 
 lemma list_of_dlist_filter [simp, code abstract]:
-  "list_of_dlist (filter P dxs) = List.filter P (list_of_dlist dxs)"
-  by (simp add: filter_def)
+  "list_of_dlist (Dlist.filter P dxs) = List.filter P (list_of_dlist dxs)"
+  by (simp add: Dlist.filter_def)
 
 
 text \<open>Explicit executable conversion\<close>
@@ -134,28 +144,29 @@
 subsection \<open>Induction principle and case distinction\<close>
 
 lemma dlist_induct [case_names empty insert, induct type: dlist]:
-  assumes empty: "P empty"
-  assumes insrt: "\<And>x dxs. \<not> member dxs x \<Longrightarrow> P dxs \<Longrightarrow> P (insert x dxs)"
+  assumes empty: "P Dlist.empty"
+  assumes insrt: "\<And>x dxs. \<not> Dlist.member dxs x \<Longrightarrow> P dxs \<Longrightarrow> P (Dlist.insert x dxs)"
   shows "P dxs"
 proof (cases dxs)
   case (Abs_dlist xs)
-  then have "distinct xs" and dxs: "dxs = Dlist xs" by (simp_all add: Dlist_def distinct_remdups_id)
+  then have "distinct xs" and dxs: "dxs = Dlist xs"
+    by (simp_all add: Dlist_def distinct_remdups_id)
   from \<open>distinct xs\<close> have "P (Dlist xs)"
   proof (induct xs)
-    case Nil from empty show ?case by (simp add: empty_def)
+    case Nil from empty show ?case by (simp add: Dlist.empty_def)
   next
     case (Cons x xs)
-    then have "\<not> member (Dlist xs) x" and "P (Dlist xs)"
-      by (simp_all add: member_def List.member_def)
-    with insrt have "P (insert x (Dlist xs))" .
-    with Cons show ?case by (simp add: insert_def distinct_remdups_id)
+    then have "\<not> Dlist.member (Dlist xs) x" and "P (Dlist xs)"
+      by (simp_all add: Dlist.member_def List.member_def)
+    with insrt have "P (Dlist.insert x (Dlist xs))" .
+    with Cons show ?case by (simp add: Dlist.insert_def distinct_remdups_id)
   qed
   with dxs show "P dxs" by simp
 qed
 
 lemma dlist_case [cases type: dlist]:
-  obtains (empty) "dxs = empty"
-    | (insert) x dys where "\<not> member dys x" and "dxs = insert x dys"
+  obtains (empty) "dxs = Dlist.empty"
+    | (insert) x dys where "\<not> Dlist.member dys x" and "dxs = Dlist.insert x dys"
 proof (cases dxs)
   case (Abs_dlist xs)
   then have dxs: "dxs = Dlist xs" and distinct: "distinct xs"
@@ -163,13 +174,13 @@
   show thesis
   proof (cases xs)
     case Nil with dxs
-    have "dxs = empty" by (simp add: empty_def) 
+    have "dxs = Dlist.empty" by (simp add: Dlist.empty_def) 
     with empty show ?thesis .
   next
     case (Cons x xs)
-    with dxs distinct have "\<not> member (Dlist xs) x"
-      and "dxs = insert x (Dlist xs)"
-      by (simp_all add: member_def List.member_def insert_def distinct_remdups_id)
+    with dxs distinct have "\<not> Dlist.member (Dlist xs) x"
+      and "dxs = Dlist.insert x (Dlist xs)"
+      by (simp_all add: Dlist.member_def List.member_def Dlist.insert_def distinct_remdups_id)
     with insert show ?thesis .
   qed
 qed
@@ -178,14 +189,11 @@
 subsection \<open>Functorial structure\<close>
 
 functor map: map
-  by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
+  by (simp_all add: remdups_map_remdups fun_eq_iff dlist_eq_iff)
 
 
 subsection \<open>Quickcheck generators\<close>
 
-quickcheck_generator dlist predicate: distinct constructors: empty, insert
-
-
-hide_const (open) member fold foldr empty insert remove map filter null member length fold
+quickcheck_generator dlist predicate: distinct constructors: Dlist.empty, Dlist.insert
 
 end
diff -r dcfc28144858 -r 3a4400985780 src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/IArray.thy	Fri Sep 04 19:22:13 2015 +0200
@@ -13,36 +13,35 @@
 lists first. Arrays could be converted back into lists for printing if they
 were wrapped up in an additional constructor.\<close>
 
+context
+begin
+
 datatype 'a iarray = IArray "'a list"
 
-primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
+qualified primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
 "list_of (IArray xs) = xs"
-hide_const (open) list_of
 
-definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
+qualified definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
 [simp]: "of_fun f n = IArray (map f [0..<n])"
-hide_const (open) of_fun
 
-definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
+qualified definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
 [simp]: "as !! n = IArray.list_of as ! n"
-hide_const (open) sub
 
-definition length :: "'a iarray \<Rightarrow> nat" where
+qualified definition length :: "'a iarray \<Rightarrow> nat" where
 [simp]: "length as = List.length (IArray.list_of as)"
-hide_const (open) length
 
-fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+qualified fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
 "all p (IArray as) = (ALL a : set as. p a)"
-hide_const (open) all
 
-fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+qualified fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
 "exists p (IArray as) = (EX a : set as. p a)"
-hide_const (open) exists
 
 lemma list_of_code [code]:
 "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
 by (cases as) (simp add: map_nth)
 
+end
+
 
 subsection "Code Generation"
 
@@ -86,10 +85,13 @@
   "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
   by (cases as, cases bs) (simp add: equal)
 
-primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
+context
+begin
+
+qualified primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
   "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
 
-hide_const (open) tabulate
+end
 
 lemma [code]:
   "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
@@ -98,10 +100,13 @@
 code_printing
   constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
 
-primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
+context
+begin
+
+qualified primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
   [code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
 
-hide_const (open) sub'
+end
 
 lemma [code]:
   "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
@@ -114,10 +119,13 @@
 code_printing
   constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
 
-definition length' :: "'a iarray \<Rightarrow> integer" where
+context
+begin
+
+qualified definition length' :: "'a iarray \<Rightarrow> integer" where
   [code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
 
-hide_const (open) length'
+end
 
 lemma [code]:
   "IArray.length' (IArray as) = integer_of_nat (List.length as)" 
diff -r dcfc28144858 -r 3a4400985780 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Fri Sep 04 16:01:58 2015 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Fri Sep 04 19:22:13 2015 +0200
@@ -314,10 +314,10 @@
 and x :: 'a
 begin
 
-fun rtrancl_while_test :: "'a list \<times> 'a set \<Rightarrow> bool"
+qualified fun rtrancl_while_test :: "'a list \<times> 'a set \<Rightarrow> bool"
 where "rtrancl_while_test (ws,_) = (ws \<noteq> [] \<and> p(hd ws))"
 
-fun rtrancl_while_step :: "'a list \<times> 'a set \<Rightarrow> 'a list \<times> 'a set"
+qualified fun rtrancl_while_step :: "'a list \<times> 'a set \<Rightarrow> 'a list \<times> 'a set"
 where "rtrancl_while_step (ws, Z) =
   (let x = hd ws; new = remdups (filter (\<lambda>y. y \<notin> Z) (f x))
   in (new @ tl ws, set new \<union> Z))"
@@ -325,12 +325,12 @@
 definition rtrancl_while :: "('a list * 'a set) option"
 where "rtrancl_while = while_option rtrancl_while_test rtrancl_while_step ([x],{x})"
 
-fun rtrancl_while_invariant :: "'a list \<times> 'a set \<Rightarrow> bool"
+qualified fun rtrancl_while_invariant :: "'a list \<times> 'a set \<Rightarrow> bool"
 where "rtrancl_while_invariant (ws, Z) =
    (x \<in> Z \<and> set ws \<subseteq> Z \<and> distinct ws \<and> {(x,y). y \<in> set(f x)} `` (Z - set ws) \<subseteq> Z \<and>
     Z \<subseteq> {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z))"
 
-lemma rtrancl_while_invariant: 
+qualified lemma rtrancl_while_invariant: 
   assumes inv: "rtrancl_while_invariant st" and test: "rtrancl_while_test st"
   shows   "rtrancl_while_invariant (rtrancl_while_step st)"
 proof (cases st)
@@ -392,7 +392,4 @@
 
 end
 
-hide_const (open) rtrancl_while_test rtrancl_while_step rtrancl_while_invariant
-hide_fact (open) rtrancl_while_invariant
-
 end