# HG changeset patch
# User wenzelm
# Date 1465559297 -7200
# Node ID ce63815d48dd2b66805071e26f0366b6ede565c0
# Parent  4f3402f35be7ecea33886364f872097350e73da8
tuned;

diff -r 4f3402f35be7 -r ce63815d48dd src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Fri Jun 10 13:18:57 2016 +0200
+++ b/src/Pure/Isar/bundle.ML	Fri Jun 10 13:48:17 2016 +0200
@@ -79,13 +79,13 @@
 fun pretty_bundle ctxt (markup_name, bundle) =
   let
     val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
-
+    fun prt_thm_attribs atts th =
+      Pretty.block (Pretty.breaks (prt_thm th :: Attrib.pretty_attribs ctxt atts));
     fun prt_thms (ths, []) = map prt_thm ths
-      | prt_thms (ths, atts) = Pretty.enclose "(" ")"
-          (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
+      | prt_thms (ths, atts) = map (prt_thm_attribs atts) ths;
   in
     Pretty.block ([Pretty.keyword1 "bundle", Pretty.str " ", Pretty.mark_str markup_name] @
-      (if null bundle then [] else Pretty.breaks (Pretty.str " =" :: maps prt_thms bundle)))
+      (if null bundle then [] else Pretty.fbreaks (Pretty.str " =" :: maps prt_thms bundle)))
   end;
 
 fun print_bundles verbose ctxt =
@@ -131,17 +131,21 @@
 
 fun bad_operation _ = error "Not possible in bundle target";
 
-fun conclude binding =
+fun conclude invisible binding =
   Local_Theory.background_theory_result (fn thy =>
-    let
-      val (name, Context.Theory thy') =
-        define_bundle (binding, the_target thy) (Context.Theory thy);
-    in (name, reset_target thy') end);
+    thy
+    |> invisible ? Context_Position.set_visible_global false
+    |> Context.Theory
+    |> define_bundle (binding, the_target thy)
+    ||> Context.the_theory
+    ||> reset_target);
 
 fun pretty binding lthy =
   let
     val bundle = the_target (Proof_Context.theory_of lthy);
-    val (name, lthy') = conclude binding lthy;
+    val (name, lthy') = lthy
+      |> Local_Theory.raw_theory (Context_Position.set_visible_global false)
+      |> conclude true binding;
     val thy_ctxt' = Proof_Context.init_global (Proof_Context.theory_of lthy');
     val markup_name =
       Name_Space.markup_extern thy_ctxt' (Name_Space.space_of_table (get_bundles thy_ctxt')) name;
@@ -179,7 +183,7 @@
       theory_registration = bad_operation,
       locale_dependency = bad_operation,
       pretty = pretty binding,
-      exit = conclude binding #> #2 #> Local_Theory.target_of #> Sign.change_end_local}
+      exit = conclude false binding #> #2 #> Local_Theory.target_of #> Sign.change_end_local}
 
 end;