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