# HG changeset patch
# User wenzelm
# Date 1461144825 -7200
# Node ID c4d2945c49003694fc8625d6ebfbca2b4a9cad27
# Parent  4e7eff53bee77085d83967cc93a0f12737b04b22
invisible context similar to interpretation;

diff -r 4e7eff53bee7 -r c4d2945c4900 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Wed Apr 20 11:14:10 2016 +0200
+++ b/src/Pure/Isar/bundle.ML	Wed Apr 20 11:33:45 2016 +0200
@@ -86,8 +86,12 @@
 local
 
 fun gen_includes get args ctxt =
-  let val decls = maps (get ctxt) args
-  in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end;
+  let val decls = maps (get ctxt) args in
+    ctxt
+    |> Context_Position.set_visible false
+    |> Attrib.local_notes "" [((Binding.empty, []), decls)] |> #2
+    |> Context_Position.restore_visible ctxt
+  end;
 
 fun gen_context get prep_decl raw_incls raw_elems gthy =
   let