# HG changeset patch
# User wenzelm
# Date 1465591645 -7200
# Node ID 7c509ddf29a517a3d9306f80572e01b8fe4be2e0
# Parent  06b021ff892023ea6b010fc04705a20f8d4ea7b9
added command 'unbundle';

diff -r 06b021ff8920 -r 7c509ddf29a5 NEWS
--- a/NEWS	Fri Jun 10 17:12:14 2016 +0100
+++ b/NEWS	Fri Jun 10 22:47:25 2016 +0200
@@ -45,6 +45,10 @@
   declare b [intro]
 end
 
+* Command 'unbundle' is like 'include', but works within a local theory
+context. Unlike "context includes ... begin", the effect of 'unbundle'
+on the target context persists, until different declarations are given.
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
diff -r 06b021ff8920 -r 7c509ddf29a5 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Fri Jun 10 17:12:14 2016 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Fri Jun 10 22:47:25 2016 +0200
@@ -253,9 +253,13 @@
   \<^descr> \<^theory_text>\<open>print_bundles\<close> prints the named bundles that are available in the
   current context; the ``\<open>!\<close>'' option indicates extra verbosity.
 
-  \<^descr> \<^theory_text>\<open>include b\<^sub>1 \<dots> b\<^sub>n\<close> includes the declarations from the given bundles into
-  the current proof body context. This is analogous to \<^theory_text>\<open>note\<close>
-  (\secref{sec:proof-facts}) with the expanded bundles.
+  \<^descr> \<^theory_text>\<open>unbundle b\<^sub>1 \<dots> b\<^sub>n\<close> activates the declarations from the given bundles in
+  the current local theory context. This is analogous to \<^theory_text>\<open>lemmas\<close>
+  (\secref{sec:theorems}) with the expanded bundles.
+
+  \<^descr> \<^theory_text>\<open>include\<close> is similar to \<^theory_text>\<open>unbundle\<close>, but works in a proof body (forward
+  mode). This is analogous to \<^theory_text>\<open>note\<close> (\secref{sec:proof-facts}) with the
+  expanded bundles.
 
   \<^descr> \<^theory_text>\<open>including\<close> is similar to \<^theory_text>\<open>include\<close>, but works in proof refinement
   (backward mode). This is analogous to \<^theory_text>\<open>using\<close> (\secref{sec:proof-facts})
diff -r 06b021ff8920 -r 7c509ddf29a5 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Fri Jun 10 17:12:14 2016 +0100
+++ b/src/Pure/Isar/bundle.ML	Fri Jun 10 22:47:25 2016 +0200
@@ -15,6 +15,8 @@
   val bundle_cmd: binding * (Facts.ref * Token.src list) list ->
     (binding * string option * mixfix) list -> local_theory -> local_theory
   val init: binding -> theory -> local_theory
+  val unbundle: string list -> local_theory -> local_theory
+  val unbundle_cmd: (xstring * Position.T) list -> local_theory -> local_theory
   val includes: string list -> Proof.context -> Proof.context
   val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
   val include_: string list -> Proof.state -> Proof.state
@@ -190,18 +192,20 @@
 
 
 
-(** include bundles **)
+(** activate bundles **)
 
 local
 
-fun gen_includes get args ctxt =
+fun gen_activate notes get args ctxt =
   let val decls = maps (get ctxt) args in
     ctxt
     |> Context_Position.set_visible false
-    |> Attrib.local_notes "" [((Binding.empty, []), decls)] |> #2
+    |> notes [((Binding.empty, []), decls)] |> #2
     |> Context_Position.restore_visible ctxt
   end;
 
+fun gen_includes get = gen_activate (Attrib.local_notes "") get;
+
 fun gen_context get prep_decl raw_incls raw_elems gthy =
   let
     val (after_close, lthy) =
@@ -217,6 +221,9 @@
 
 in
 
+val unbundle = gen_activate Local_Theory.notes get_bundle;
+val unbundle_cmd = gen_activate Local_Theory.notes get_bundle_cmd;
+
 val includes = gen_includes get_bundle;
 val includes_cmd = gen_includes get_bundle_cmd;
 
diff -r 06b021ff8920 -r 7c509ddf29a5 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri Jun 10 17:12:14 2016 +0100
+++ b/src/Pure/Pure.thy	Fri Jun 10 22:47:25 2016 +0200
@@ -32,6 +32,7 @@
     "parse_ast_translation" "parse_translation" "print_translation"
     "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
   and "bundle" :: thy_decl_block
+  and "unbundle" :: thy_decl
   and "include" "including" :: prf_decl
   and "print_bundles" :: diag
   and "context" "locale" "experiment" :: thy_decl_block
@@ -498,13 +499,18 @@
     (Parse.binding --| Parse.begin >> Bundle.init);
 
 val _ =
+  Outer_Syntax.local_theory @{command_keyword unbundle}
+    "activate declarations from bundle in local theory"
+    (Scan.repeat1 (Parse.position Parse.name) >> Bundle.unbundle_cmd);
+
+val _ =
   Outer_Syntax.command @{command_keyword include}
-    "include declarations from bundle in proof body"
+    "activate declarations from bundle in proof body"
     (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.include_cmd));
 
 val _ =
   Outer_Syntax.command @{command_keyword including}
-    "include declarations from bundle in goal refinement"
+    "activate declarations from bundle in goal refinement"
     (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.including_cmd));
 
 val _ =