# HG changeset patch
# User wenzelm
# Date 1428085399 -7200
# Node ID fe1d8576b48308470d2838a50ad8133f336c99b6
# Parent  d01e6d159c33b7985535120f6d2619b595771196
clarified name space policy: show less stuff in usual print functions;

diff -r d01e6d159c33 -r fe1d8576b483 src/Pure/Isar/experiment.ML
--- a/src/Pure/Isar/experiment.ML	Fri Apr 03 20:04:16 2015 +0200
+++ b/src/Pure/Isar/experiment.ML	Fri Apr 03 20:23:19 2015 +0200
@@ -15,12 +15,14 @@
 
 fun gen_experiment add_locale elems thy =
   let
-    val (_, lthy) = thy
-      |> add_locale (Binding.name ("experiment" ^ serial_string ())) Binding.empty ([], []) elems;
+    val experiment_name = Binding.name ("experiment" ^ serial_string ()) |> Binding.concealed;
+    val (_, lthy) = thy |> add_locale experiment_name Binding.empty ([], []) elems;
     val (scope, naming) =
       Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
     val naming' = naming |> Name_Space.private scope;
-    val lthy' = lthy |> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming')));
+    val lthy' = lthy
+      |> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming')))
+      |> Local_Theory.map_background_naming Name_Space.concealed;
   in (scope, lthy') end;
 
 val experiment = gen_experiment Expression.add_locale;