src/Pure/Isar/bundle.ML

   val bundle: binding * Attrib.thms ->
     (binding * typ option * mixfix) list -> local_theory -> local_theory
   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
   val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
   val including: string list -> Proof.state -> Proof.state

 
 end;
 
 
 
-(** 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) =
       gthy |> Context.cases (pair Local_Theory.exit o Named_Target.theory_init)

       (Local_Theory.background_naming_of lthy) (Local_Theory.operations_of lthy) after_close
   end;
 
 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;
 
 fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts;
 fun include_cmd bs =