src/Pure/Isar/bundle.ML

--- a/src/Pure/Isar/bundle.ML	Wed Mar 21 21:24:13 2012 +0100
+++ b/src/Pure/Isar/bundle.ML	Wed Mar 21 23:26:35 2012 +0100
@@ -15,12 +15,12 @@
     (binding * string option * mixfix) 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 context_includes: string list -> generic_theory -> local_theory
+  val context_includes_cmd: (xstring * Position.T) list -> generic_theory -> local_theory
   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
   val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
-  val context_includes: string list -> local_theory -> local_theory
-  val context_includes_cmd: (xstring * Position.T) list -> local_theory -> local_theory
   val print_bundles: Proof.context -> unit
 end;
 
@@ -93,16 +93,22 @@
     val note = ((Binding.empty, []), map (apsnd (map attrib)) decls);
   in #2 (Proof_Context.note_thmss "" [note] ctxt) end;
 
-fun gen_context prep args lthy =
-  Named_Target.assert lthy
-  |> gen_includes prep args
-  |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
+fun gen_context prep args (Context.Theory thy) =
+      Named_Target.theory_init thy
+      |> Local_Theory.target (gen_includes prep args)
+  | gen_context prep args (Context.Proof lthy) =
+      Named_Target.assert lthy
+      |> gen_includes prep args
+      |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
 
 in
 
 val includes = gen_includes (K I);
 val includes_cmd = gen_includes check;
 
+val context_includes = gen_context (K I);
+val context_includes_cmd = gen_context check;
+
 fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts;
 fun include_cmd bs =
   Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts;
@@ -110,9 +116,6 @@
 fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
 fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
 
-val context_includes = gen_context (K I);
-val context_includes_cmd = gen_context check;
-
 end;