# HG changeset patch
# User wenzelm
# Date 1332369682 -3600
# Node ID 3031603233e3eedbf8a2796b1237c6467bb0652e
# Parent  f4838ce57772056f8907652360a7bccba07df3aa# Parent  15cd66da537fe04246f7fd5ed25dd9e375085881
merged

diff -r f4838ce57772 -r 3031603233e3 Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Wed Mar 21 16:53:24 2012 +0100
+++ b/Admin/isatest/isatest-makedist	Wed Mar 21 23:41:22 2012 +0100
@@ -108,8 +108,8 @@
 $SSH macbroy24 "$MAKEALL $HOME/settings/at64-poly"
 sleep 15
 $SSH macbroy2 "
-  $MAKEALL $HOME/settings/mac-poly64-M4 -l . full;
-  $MAKEALL $HOME/settings/mac-poly64-M8 -l . full;
+  $MAKEALL -l . full $HOME/settings/mac-poly64-M4;
+  $MAKEALL -l . full $HOME/settings/mac-poly64-M8;
   $MAKEALL $HOME/settings/mac-poly-M4;
   $MAKEALL $HOME/settings/mac-poly-M8"
 sleep 15
diff -r f4838ce57772 -r 3031603233e3 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Wed Mar 21 16:53:24 2012 +0100
+++ b/etc/isar-keywords-ZF.el	Wed Mar 21 23:41:22 2012 +0100
@@ -226,6 +226,7 @@
     "if"
     "imports"
     "in"
+    "includes"
     "induction"
     "infix"
     "infixl"
diff -r f4838ce57772 -r 3031603233e3 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Wed Mar 21 16:53:24 2012 +0100
+++ b/etc/isar-keywords.el	Wed Mar 21 23:41:22 2012 +0100
@@ -305,6 +305,7 @@
     "if"
     "imports"
     "in"
+    "includes"
     "infix"
     "infixl"
     "infixr"
diff -r f4838ce57772 -r 3031603233e3 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -341,7 +341,7 @@
   let
     fun default_prover_name () =
       hd (#provers (Sledgehammer_Isar.default_params ctxt []))
-      handle Empty => error "No ATP available."
+      handle List.Empty => error "No ATP available."
     fun get_prover name =
       (name, Sledgehammer_Run.get_minimizing_prover ctxt
                 Sledgehammer_Provers.Normal name)
diff -r f4838ce57772 -r 3031603233e3 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -83,7 +83,7 @@
    (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
    rtac fs_name_thm 1 THEN
    etac exE 1) thm
-  handle Empty  => all_tac thm (* if we collected no variables then we do nothing *)
+  handle List.Empty  => all_tac thm (* if we collected no variables then we do nothing *)
   end;
 
 fun get_inner_fresh_fun (Bound j) = NONE
diff -r f4838ce57772 -r 3031603233e3 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -61,7 +61,7 @@
     Specification.theorem Thm.theoremK NONE
       (fn thmss => (Local_Theory.background_theory
          (SPARK_VCs.mark_proved vc_name (flat thmss))))
-      (Binding.name vc_name, []) ctxt stmt true lthy
+      (Binding.name vc_name, []) [] ctxt stmt true lthy
   end;
 
 fun string_of_status NONE = "(unproved)"
diff -r f4838ce57772 -r 3031603233e3 src/HOL/Tools/Function/pat_completeness.ML
--- a/src/HOL/Tools/Function/pat_completeness.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/HOL/Tools/Function/pat_completeness.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -143,7 +143,7 @@
 
     val (qss, x_pats) = split_list (map pat_of cases)
     val xs = map fst (hd x_pats)
-      handle Empty => raise COMPLETENESS
+      handle List.Empty => raise COMPLETENESS
 
     val patss = map (map snd) x_pats
     val complete_thm = prove_completeness thy xs thesis qss patss
diff -r f4838ce57772 -r 3031603233e3 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -505,7 +505,7 @@
       (case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
            [_] => [pred_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
          | xs => map (pred_of o fst o HOLogic.dest_imp) xs)
-         handle TERM _ => err () | Empty => err ();
+         handle TERM _ => err () | List.Empty => err ();
   in 
     add_ind_realizers (hd sets)
       (case arg of
diff -r f4838ce57772 -r 3031603233e3 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/HOL/Tools/recdef.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -266,7 +266,7 @@
         " in recdef definition of " ^ quote name);
   in
     Specification.theorem "" NONE (K I)
-      (Binding.conceal (Binding.name bname), atts) []
+      (Binding.conceal (Binding.name bname), atts) [] []
       (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
   end;
 
diff -r f4838ce57772 -r 3031603233e3 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -384,7 +384,7 @@
 fun extract_first p =
   let
     fun extract xs (y::ys) = if p y then (y, xs @ ys) else extract (y::xs) ys
-      | extract xs [] = raise Empty
+      | extract xs [] = raise List.Empty
   in extract [] end;
 
 fun print_ineqs ctxt ineqs =
diff -r f4838ce57772 -r 3031603233e3 src/Pure/General/balanced_tree.ML
--- a/src/Pure/General/balanced_tree.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/General/balanced_tree.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -15,7 +15,7 @@
 structure Balanced_Tree: BALANCED_TREE =
 struct
 
-fun make _ [] = raise Empty
+fun make _ [] = raise List.Empty
   | make _ [x] = x
   | make f xs =
       let
@@ -24,7 +24,7 @@
       in f (make f ps, make f qs) end;
 
 fun dest f n x =
-  if n <= 0 then raise Empty
+  if n <= 0 then raise List.Empty
   else if n = 1 then [x]
   else
     let
diff -r f4838ce57772 -r 3031603233e3 src/Pure/General/queue.ML
--- a/src/Pure/General/queue.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/General/queue.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -11,7 +11,7 @@
   val is_empty: 'a T -> bool
   val content: 'a T -> 'a list
   val enqueue: 'a -> 'a T -> 'a T
-  val dequeue: 'a T -> 'a * 'a T
+  val dequeue: 'a T -> 'a * 'a T  (*exception List.Empty*)
 end;
 
 structure Queue: QUEUE =
@@ -30,6 +30,6 @@
 
 fun dequeue (Queue (xs, y :: ys)) = (y, Queue (xs, ys))
   | dequeue (Queue (xs as _ :: _, [])) = let val y :: ys = rev xs in (y, Queue ([], ys)) end
-  | dequeue (Queue ([], [])) = raise Empty;
+  | dequeue (Queue ([], [])) = raise List.Empty;
 
 end;
diff -r f4838ce57772 -r 3031603233e3 src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/General/seq.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -167,7 +167,7 @@
 fun lift f xq y = map (fn x => f x y) xq;
 fun lifts f xq y = maps (fn x => f x y) xq;
 
-fun singleton f x = f [x] |> map (fn [y] => y | _ => raise Empty);
+fun singleton f x = f [x] |> map (fn [y] => y | _ => raise List.Empty);
 
 (*print a sequence, up to "count" elements*)
 fun print print_elem count =
diff -r f4838ce57772 -r 3031603233e3 src/Pure/General/stack.ML
--- a/src/Pure/General/stack.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/General/stack.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -13,7 +13,7 @@
   val map_top: ('a -> 'a) -> 'a T -> 'a T
   val map_all: ('a -> 'a) -> 'a T -> 'a T
   val push: 'a T -> 'a T
-  val pop: 'a T -> 'a T      (*exception Empty*)
+  val pop: 'a T -> 'a T      (*exception List.Empty*)
 end;
 
 structure Stack: STACK =
@@ -34,6 +34,6 @@
 fun push (x, xs) = (x, x :: xs);
 
 fun pop (_, x :: xs) = (x, xs)
-  | pop (_, []) = raise Empty;
+  | pop (_, []) = raise List.Empty;
 
 end;
diff -r f4838ce57772 -r 3031603233e3 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/bundle.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -13,10 +13,14 @@
     (binding * typ option * mixfix) list -> local_theory -> local_theory
   val bundle_cmd: binding * (Facts.ref * Args.src list) list ->
     (binding * string option * mixfix) list -> local_theory -> local_theory
-  val include_: string -> Proof.state -> Proof.state
-  val include_cmd: xstring * Position.T -> Proof.state -> Proof.state
-  val including: string -> Proof.state -> Proof.state
-  val including_cmd: xstring * Position.T -> Proof.state -> Proof.state
+  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 print_bundles: Proof.context -> unit
 end;
 
@@ -78,20 +82,42 @@
 end;
 
 
-(* include bundle *)
+(* include bundles *)
+
+local
+
+fun gen_includes prep args ctxt =
+  let
+    val decls = maps (the_bundle ctxt o prep ctxt) args;
+    val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
+    val note = ((Binding.empty, []), map (apsnd (map attrib)) decls);
+  in #2 (Proof_Context.note_thmss "" [note] ctxt) end;
 
-fun gen_include prep raw_name =
-  Proof.map_context (fn ctxt =>
-    let
-      val bundle = the_bundle ctxt (prep ctxt raw_name);
-      val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
-      val note = ((Binding.empty, []), map (apsnd (map attrib)) bundle);
-    in #2 (Proof_Context.note_thmss "" [note] ctxt) end);
+fun gen_context prep args (Context.Theory thy) =
+      Named_Target.theory_init thy
+      |> Local_Theory.target (gen_includes prep args)
+      |> Local_Theory.restore
+  | 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
 
-fun include_ name = Proof.assert_forward #> gen_include (K I) name #> Proof.put_facts NONE;
-fun include_cmd name = Proof.assert_forward #> gen_include check name #> Proof.put_facts NONE;
-fun including name = Proof.assert_backward #> gen_include (K I) name;
-fun including_cmd name = Proof.assert_backward #> gen_include check name;
+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;
+
+fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
+fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
+
+end;
 
 
 (* print_bundles *)
diff -r f4838ce57772 -r 3031603233e3 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/class.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -512,6 +512,8 @@
 
 fun instantiation (tycos, vs, sort) thy =
   let
+    val naming = Sign.naming_of thy;
+
     val _ = if null tycos then error "At least one arity must be given" else ();
     val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort);
     fun get_param tyco (param, (_, (c, ty))) =
@@ -545,7 +547,7 @@
     |> Overloading.activate_improvable_syntax
     |> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
     |> synchronize_inst_syntax
-    |> Local_Theory.init NONE ""
+    |> Local_Theory.init naming
        {define = Generic_Target.define foundation,
         notes = Generic_Target.notes
           (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
diff -r f4838ce57772 -r 3031603233e3 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -860,7 +860,7 @@
     fun after_qed witss eqns =
       (Proof.map_context o Context.proof_map)
         (note_eqns_register deps witss attrss eqns export export')
-      #> Proof.put_facts NONE;
+      #> Proof.reset_facts;
   in
     state
     |> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int
diff -r f4838ce57772 -r 3031603233e3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -16,7 +16,7 @@
     "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
     "advanced", "and", "assumes", "attach", "begin", "binder",
     "constrains", "defines", "fixes", "for", "identifier", "if",
-    "imports", "in", "infix", "infixl", "infixr", "is", "keywords",
+    "imports", "in", "includes", "infix", "infixl", "infixr", "is", "keywords",
     "notes", "obtains", "open", "output", "overloaded", "pervasive",
     "shows", "structure", "unchecked", "uses", "where", "|"]));
 
@@ -25,16 +25,17 @@
 (** init and exit **)
 
 val _ =
-  Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory"
+  Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory context"
     (Thy_Header.args >> (fn header =>
       Toplevel.print o
         Toplevel.init_theory
           (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
 
 val _ =
-  Outer_Syntax.command ("end", Keyword.tag_theory Keyword.thy_end) "end (local) theory"
+  Outer_Syntax.command ("end", Keyword.tag_theory Keyword.thy_end) "end context"
     (Scan.succeed
-      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.end_proof (K Proof.end_notepad)));
+      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
+        Toplevel.end_proof (K Proof.end_notepad)));
 
 
 
@@ -406,14 +407,6 @@
       (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
 
 
-(* local theories *)
-
-val _ =
-  Outer_Syntax.command ("context", Keyword.thy_decl) "enter local theory context"
-    (Parse.position Parse.xname --| Parse.begin >> (fn name =>
-      Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
-
-
 (* bundled declarations *)
 
 val _ =
@@ -424,12 +417,14 @@
 val _ =
   Outer_Syntax.command ("include", Keyword.prf_decl)
     "include declarations from bundle in proof body"
-    (Parse.position Parse.xname >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
+    (Scan.repeat1 (Parse.position Parse.xname)
+      >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
 
 val _ =
   Outer_Syntax.command ("including", Keyword.prf_decl)
     "include declarations from bundle in goal refinement"
-    (Parse.position Parse.xname >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
+    (Scan.repeat1 (Parse.position Parse.xname)
+      >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
 
 val _ =
   Outer_Syntax.improper_command ("print_bundles", Keyword.diag) "print bundles of declarations"
@@ -437,6 +432,16 @@
       Toplevel.keep (Bundle.print_bundles o Toplevel.context_of)));
 
 
+(* local theories *)
+
+val _ =
+  Outer_Syntax.command ("context", Keyword.thy_decl) "begin local theory context"
+    ((Parse_Spec.includes >> (Toplevel.open_target o Bundle.context_includes_cmd) ||
+      Parse.position Parse.xname >> (fn name =>
+        Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)))
+      --| Parse.begin);
+
+
 (* locales *)
 
 val locale_val =
@@ -544,10 +549,12 @@
      else (kind, Keyword.thy_goal))
     ("state " ^ (if schematic then "schematic " ^ kind else kind))
     (Scan.optional (Parse_Spec.opt_thm_name ":" --|
-      Scan.ahead (Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
-      Parse_Spec.general_statement >> (fn (a, (elems, concl)) =>
+      Scan.ahead (Parse_Spec.includes >> K "" ||
+        Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
+      Scan.optional Parse_Spec.includes [] --
+      Parse_Spec.general_statement >> (fn ((a, includes), (elems, concl)) =>
         ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
-          kind NONE (K I) a elems concl)));
+          kind NONE (K I) a includes elems concl)));
 
 val _ = gen_theorem false Thm.theoremK;
 val _ = gen_theorem false Thm.lemmaK;
@@ -557,8 +564,7 @@
 val _ = gen_theorem true Thm.corollaryK;
 
 val _ =
-  Outer_Syntax.local_theory_to_proof ("notepad", Keyword.thy_decl)
-    "Isar proof state as formal notepad, without any result"
+  Outer_Syntax.local_theory_to_proof ("notepad", Keyword.thy_decl) "begin proof context"
     (Parse.begin >> K Proof.begin_notepad);
 
 val _ =
diff -r f4838ce57772 -r 3031603233e3 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/local_defs.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -173,7 +173,7 @@
 
 val is_trivial = Pattern.aeconv o Logic.dest_equals o Thm.prop_of;
 
-fun trans_list _ _ [] = raise Empty
+fun trans_list _ _ [] = raise List.Empty
   | trans_list trans ctxt (th :: raw_eqs) =
       (case filter_out is_trivial raw_eqs of
         [] => th
diff -r f4838ce57772 -r 3031603233e3 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/local_theory.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -10,7 +10,12 @@
 signature LOCAL_THEORY =
 sig
   type operations
-  val affirm: local_theory -> local_theory
+  val map_contexts: (Proof.context -> Proof.context) -> local_theory -> local_theory
+  val assert: local_theory -> local_theory
+  val level: Proof.context -> int
+  val assert_bottom: bool -> local_theory -> local_theory
+  val open_target: Name_Space.naming -> operations -> local_theory -> local_theory
+  val close_target: local_theory -> local_theory
   val naming_of: local_theory -> Name_Space.naming
   val full_name: local_theory -> binding -> string
   val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
@@ -25,11 +30,11 @@
   val background_theory: (theory -> theory) -> local_theory -> local_theory
   val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
-  val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
   val propagate_ml_env: generic_theory -> generic_theory
   val standard_morphism: local_theory -> Proof.context -> morphism
   val target_morphism: local_theory -> morphism
   val global_morphism: local_theory -> morphism
+  val operations_of: local_theory -> operations
   val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
@@ -49,7 +54,7 @@
   val class_alias: binding -> class -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
-  val init: serial option -> string -> operations -> Proof.context -> local_theory
+  val init: Name_Space.naming -> operations -> Proof.context -> local_theory
   val restore: local_theory -> local_theory
   val exit: local_theory -> Proof.context
   val exit_global: local_theory -> theory
@@ -76,35 +81,56 @@
   pretty: local_theory -> Pretty.T list,
   exit: local_theory -> Proof.context};
 
-datatype lthy = LThy of
+type lthy =
  {naming: Name_Space.naming,
-  theory_prefix: string,
   operations: operations,
   target: Proof.context};
 
-fun make_lthy (naming, theory_prefix, operations, target) =
-  LThy {naming = naming, theory_prefix = theory_prefix,
-    operations = operations, target = target};
+fun make_lthy (naming, operations, target) : lthy =
+  {naming = naming, operations = operations, target = target};
 
 
 (* context data *)
 
 structure Data = Proof_Data
 (
-  type T = lthy option;
-  fun init _ = NONE;
+  type T = lthy list;
+  fun init _ = [];
 );
 
-fun get_lthy lthy =
-  (case Data.get lthy of
-    NONE => error "No local theory context"
-  | SOME (LThy data) => data);
+fun map_contexts f =
+  (Data.map o map) (fn {naming, operations, target} => make_lthy (naming, operations, f target))
+  #> f;
+
+fun assert lthy =
+  if null (Data.get lthy) then error "Missing local theory context" else lthy;
+
+val get_lthy = hd o Data.get o assert;
+
+fun map_lthy f = assert #>
+  Data.map (fn {naming, operations, target} :: parents =>
+    make_lthy (f (naming, operations, target)) :: parents);
+
+
+(* nested structure *)
 
-fun map_lthy f lthy =
-  let val {naming, theory_prefix, operations, target} = get_lthy lthy
-  in Data.put (SOME (make_lthy (f (naming, theory_prefix, operations, target)))) lthy end;
+val level = length o Data.get;
 
-val affirm = tap get_lthy;
+fun assert_bottom b lthy =
+  let
+    val _ = assert lthy;
+    val b' = level lthy <= 1;
+  in
+    if b andalso not b' then error "Not at bottom of local theory nesting"
+    else if not b andalso b' then error "Already at bottom of local theory nesting"
+    else lthy
+  end;
+
+fun open_target naming operations target = assert target
+  |> Data.map (cons (make_lthy (naming, operations, target)));
+
+fun close_target lthy =
+  assert_bottom false lthy |> Data.map tl;
 
 
 (* naming *)
@@ -112,8 +138,7 @@
 val naming_of = #naming o get_lthy;
 val full_name = Name_Space.full_name o naming_of;
 
-fun map_naming f = map_lthy (fn (naming, theory_prefix, operations, target) =>
-  (f naming, theory_prefix, operations, target));
+fun map_naming f = map_lthy (fn (naming, operations, target) => (f naming, operations, target));
 
 val conceal = map_naming Name_Space.conceal;
 val new_group = map_naming Name_Space.new_group;
@@ -126,8 +151,7 @@
 
 val target_of = #target o get_lthy;
 
-fun map_target f = map_lthy (fn (naming, theory_prefix, operations, target) =>
-  (naming, theory_prefix, operations, f target));
+fun map_target f = map_lthy (fn (naming, operations, target) => (naming, operations, f target));
 
 
 (* substructure mappings *)
@@ -135,9 +159,7 @@
 fun raw_theory_result f lthy =
   let
     val (res, thy') = f (Proof_Context.theory_of lthy);
-    val lthy' = lthy
-      |> map_target (Proof_Context.transfer thy')
-      |> Proof_Context.transfer thy';
+    val lthy' = map_contexts (Proof_Context.transfer thy') lthy;
   in (res, lthy') end;
 
 fun raw_theory f = #2 o raw_theory_result (f #> pair ());
@@ -163,18 +185,18 @@
     val thy' = Proof_Context.theory_of ctxt';
     val lthy' = lthy
       |> map_target (K ctxt')
-      |> Proof_Context.transfer thy';
+      |> map_contexts (Proof_Context.transfer thy');
   in (res, lthy') end;
 
 fun target f = #2 o target_result (f #> pair ());
 
-fun map_contexts f =
-  background_theory (Context.theory_map f) #>
-  target (Context.proof_map f) #>
-  Context.proof_map f;
-
 fun propagate_ml_env (context as Context.Proof lthy) =
-      Context.Proof (map_contexts (ML_Env.inherit context) lthy)
+      let val inherit = ML_Env.inherit context in
+        lthy
+        |> background_theory (Context.theory_map inherit)
+        |> map_contexts (Context.proof_map inherit)
+        |> Context.Proof
+      end
   | propagate_ml_env context = context;
 
 
@@ -185,15 +207,21 @@
   Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
 
 fun target_morphism lthy = standard_morphism lthy (target_of lthy);
+
 fun global_morphism lthy =
   standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
 
 
-(* primitive operations *)
+
+(** operations **)
+
+val operations_of = #operations o get_lthy;
 
-fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
-fun operation1 f x = operation (fn ops => f ops x);
-fun operation2 f x y lthy = operation (fn ops => f ops x y) lthy;
+
+(* primitives *)
+
+fun operation f lthy = f (operations_of lthy) lthy;
+fun operation2 f x y = operation (fn ops => f ops x y);
 
 val pretty = operation #pretty;
 val abbrev = apsnd checkpoint ooo operation2 #abbrev;
@@ -203,8 +231,7 @@
 val declaration = checkpoint ooo operation2 #declaration;
 
 
-
-(** basic derived operations **)
+(* basic derived operations *)
 
 val notes = notes_kind "";
 fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
@@ -246,21 +273,15 @@
 
 (* init *)
 
-fun init group theory_prefix operations target =
-  let val naming =
-    Sign.naming_of (Proof_Context.theory_of target)
-    |> Name_Space.set_group group
-    |> Name_Space.mandatory_path theory_prefix;
-  in
-    target |> Data.map
-      (fn NONE => SOME (make_lthy (naming, theory_prefix, operations, target))
-        | SOME _ => error "Local theory already initialized")
-    |> checkpoint
-  end;
+fun init naming operations target =
+  target |> Data.map
+    (fn [] => [make_lthy (naming, operations, target)]
+      | _ => error "Local theory already initialized")
+  |> checkpoint;
 
 fun restore lthy =
-  let val {naming, theory_prefix, operations, target} = get_lthy lthy
-  in init (Name_Space.get_group naming) theory_prefix operations target end;
+  let val {naming, operations, target} = get_lthy lthy
+  in init naming operations target end;
 
 
 (* exit *)
diff -r f4838ce57772 -r 3031603233e3 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/named_target.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -2,16 +2,17 @@
     Author:     Makarius
     Author:     Florian Haftmann, TU Muenchen
 
-Targets for theory, locale and class.
+Targets for theory, locale, class -- at the bottom the nested structure.
 *)
 
 signature NAMED_TARGET =
 sig
+  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
+  val assert: local_theory -> local_theory
   val init: (local_theory -> local_theory) -> string -> theory -> local_theory
   val theory_init: theory -> local_theory
   val reinit: local_theory -> local_theory -> local_theory
   val context_cmd: xstring * Position.T -> theory -> local_theory
-  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
 end;
 
 structure Named_Target: NAMED_TARGET =
@@ -43,6 +44,10 @@
   Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
     {target = target, is_locale = is_locale, is_class = is_class});
 
+fun assert lthy =
+  if is_some (peek lthy) then lthy
+  else error "Not in a named target (global theory, locale, class)";
+
 
 (* generic declarations *)
 
@@ -192,11 +197,13 @@
 fun init before_exit target thy =
   let
     val ta = named_target thy target before_exit;
+    val naming = Sign.naming_of thy
+      |> Name_Space.mandatory_path (Long_Name.base_name target);
   in
     thy
     |> init_context ta
     |> Data.put (SOME ta)
-    |> Local_Theory.init NONE (Long_Name.base_name target)
+    |> Local_Theory.init naming
        {define = Generic_Target.define (target_foundation ta),
         notes = Generic_Target.notes (target_notes ta),
         abbrev = Generic_Target.abbrev (target_abbrev ta),
@@ -207,11 +214,9 @@
 
 val theory_init = init I "";
 
-fun reinit lthy =
-  (case Data.get lthy of
-    SOME (Target {target, before_exit, ...}) =>
-      init before_exit target o Local_Theory.exit_global
-  | NONE => error "Not in a named target");
+val reinit =
+  Local_Theory.assert_bottom true #> Data.get #> the #>
+  (fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target);
 
 fun context_cmd ("-", _) thy = init I "" thy
   | context_cmd target thy = init I (Locale.check thy target) thy;
diff -r f4838ce57772 -r 3031603233e3 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/overloading.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -189,6 +189,7 @@
 fun gen_overloading prep_const raw_overloading thy =
   let
     val ctxt = Proof_Context.init_global thy;
+    val naming = Sign.naming_of thy;
     val _ = if null raw_overloading then error "At least one parameter must be given" else ();
     val overloading = raw_overloading |> map (fn (v, const, checked) =>
       (Term.dest_Const (prep_const ctxt const), (v, checked)));
@@ -200,7 +201,7 @@
     |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
     |> activate_improvable_syntax
     |> synchronize_syntax
-    |> Local_Theory.init NONE ""
+    |> Local_Theory.init naming
        {define = Generic_Target.define foundation,
         notes = Generic_Target.notes
           (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
diff -r f4838ce57772 -r 3031603233e3 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/parse_spec.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -19,6 +19,7 @@
   val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
   val constdecl: (binding * string option * mixfix) parser
   val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
+  val includes: (xstring * Position.T) list parser
   val locale_mixfix: mixfix parser
   val locale_fixes: (binding * string option * mixfix) list parser
   val locale_insts: (string option list * (Attrib.binding * string) list) parser
@@ -79,6 +80,8 @@
 
 (* locale and context elements *)
 
+val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.xname));
+
 val locale_mixfix =
   Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
   Parse.mixfix;
diff -r f4838ce57772 -r 3031603233e3 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -23,7 +23,8 @@
   val put_thms: bool -> string * thm list option -> state -> state
   val the_facts: state -> thm list
   val the_fact: state -> thm
-  val put_facts: thm list option -> state -> state
+  val set_facts: thm list -> state -> state
+  val reset_facts: state -> state
   val assert_forward: state -> state
   val assert_chain: state -> state
   val assert_forward_or_chain: state -> state
@@ -183,14 +184,14 @@
 fun open_block (State st) = State (Stack.push st);
 
 fun close_block (State st) = State (Stack.pop st)
-  handle Empty => error "Unbalanced block parentheses";
+  handle List.Empty => error "Unbalanced block parentheses";
 
 fun level (State st) = Stack.level st;
 
 fun assert_bottom b state =
-  let val b' = (level state <= 2) in
-    if b andalso not b' then error "Not at bottom of proof!"
-    else if not b andalso b' then error "Already at bottom of proof!"
+  let val b' = level state <= 2 in
+    if b andalso not b' then error "Not at bottom of proof"
+    else if not b andalso b' then error "Already at bottom of proof"
     else state
   end;
 
@@ -231,16 +232,19 @@
   map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
   put_thms true (Auto_Bind.thisN, facts);
 
+val set_facts = put_facts o SOME;
+val reset_facts = put_facts NONE;
+
 fun these_factss more_facts (named_factss, state) =
-  (named_factss, state |> put_facts (SOME (maps snd named_factss @ more_facts)));
+  (named_factss, state |> set_facts (maps snd named_factss @ more_facts));
 
 fun export_facts inner outer =
   (case get_facts inner of
-    NONE => put_facts NONE outer
+    NONE => reset_facts outer
   | SOME thms =>
       thms
       |> Proof_Context.export (context_of inner) (context_of outer)
-      |> (fn ths => put_facts (SOME ths) outer));
+      |> (fn ths => set_facts ths outer));
 
 
 (* mode *)
@@ -272,17 +276,20 @@
 fun current_goal state =
   (case current state of
     {context, goal = SOME (Goal goal), ...} => (context, goal)
-  | _ => error "No current goal!");
+  | _ => error "No current goal");
 
 fun assert_current_goal g state =
   let val g' = can current_goal state in
-    if g andalso not g' then error "No goal in this block!"
-    else if not g andalso g' then error "Goal present in this block!"
+    if g andalso not g' then error "No goal in this block"
+    else if not g andalso g' then error "Goal present in this block"
     else state
   end;
 
 fun put_goal goal = map_current (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
 
+val set_goal = put_goal o SOME;
+val reset_goal = put_goal NONE;
+
 val before_qed = #before_qed o #2 o current_goal;
 
 
@@ -298,7 +305,7 @@
       in map_context f (State (nd, node' :: nodes')) end
   | map_goal _ _ state = state;
 
-fun set_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) =>
+fun provide_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) =>
   (statement, [], using, goal, before_qed, after_qed));
 
 fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) =>
@@ -412,10 +419,10 @@
   |> ALLGOALS Goal.conjunction_tac
   |> Seq.maps (fn goal =>
     state
-    |> Seq.lift set_goal (Goal.extract 1 n goal |> Seq.maps (Goal.conjunction_tac 1))
+    |> Seq.lift provide_goal (Goal.extract 1 n goal |> Seq.maps (Goal.conjunction_tac 1))
     |> Seq.maps meth
     |> Seq.maps (fn state' => state'
-      |> Seq.lift set_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
+      |> Seq.lift provide_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
     |> Seq.maps (apply_method true (K Method.succeed)));
 
 fun apply_text cc text state =
@@ -471,7 +478,7 @@
   in
     raw_rules
     |> Proof_Context.goal_export inner outer
-    |> (fn rules => Seq.lift set_goal (EVERY (map refine rules) goal) state)
+    |> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state)
   end;
 
 end;
@@ -488,7 +495,7 @@
     val ngoals = Thm.nprems_of goal;
     val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
       (Goal_Display.pretty_goals ctxt goal @
-        [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])));
+        [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)")])));
 
     val extra_hyps = Assumption.extra_hyps ctxt goal;
     val _ = null extra_hyps orelse
@@ -548,7 +555,7 @@
   state
   |> assert_forward
   |> map_context (bind true args #> snd)
-  |> put_facts NONE;
+  |> reset_facts;
 
 in
 
@@ -565,7 +572,7 @@
 fun gen_write prep_arg mode args =
   assert_forward
   #> map_context (fn ctxt => ctxt |> Proof_Context.notation true mode (map (prep_arg ctxt) args))
-  #> put_facts NONE;
+  #> reset_facts;
 
 in
 
@@ -585,7 +592,7 @@
 fun gen_fix prep_vars args =
   assert_forward
   #> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (prep_vars args ctxt)) ctxt))
-  #> put_facts NONE;
+  #> reset_facts;
 
 in
 
@@ -635,7 +642,7 @@
     |-> (fn vars =>
       map_context_result (prep_binds false (map swap raw_rhss))
       #-> (fn rhss => map_context_result (Local_Defs.add_defs (vars ~~ (name_atts ~~ rhss)))))
-    |-> (put_facts o SOME o map (#2 o #2))
+    |-> (set_facts o map (#2 o #2))
   end;
 
 in
@@ -652,7 +659,7 @@
 (* chain *)
 
 fun clean_facts ctxt =
-  put_facts (SOME (filter_out Thm.is_dummy (the_facts ctxt))) ctxt;
+  set_facts (filter_out Thm.is_dummy (the_facts ctxt)) ctxt;
 
 val chain =
   assert_forward
@@ -660,7 +667,7 @@
   #> enter_chain;
 
 fun chain_facts facts =
-  put_facts (SOME facts)
+  set_facts facts
   #> chain;
 
 
@@ -765,15 +772,15 @@
 val begin_block =
   assert_forward
   #> open_block
-  #> put_goal NONE
+  #> reset_goal
   #> open_block;
 
 val next_block =
   assert_forward
   #> close_block
   #> open_block
-  #> put_goal NONE
-  #> put_facts NONE;
+  #> reset_goal
+  #> reset_facts;
 
 fun end_block state =
   state
@@ -889,12 +896,12 @@
   in
     goal_state
     |> map_context (init_context #> Variable.set_body true)
-    |> put_goal (SOME (make_goal (statement, [], [], Goal.init goal, before_qed, after_qed')))
+    |> set_goal (make_goal (statement, [], [], Goal.init goal, before_qed, after_qed'))
     |> map_context (Proof_Context.auto_bind_goal props)
     |> chaining ? (`the_facts #-> using_facts)
-    |> put_facts NONE
+    |> reset_facts
     |> open_block
-    |> put_goal NONE
+    |> reset_goal
     |> enter_backward
     |> not (null vars) ? refine_terms (length goal_propss)
     |> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
diff -r f4838ce57772 -r 3031603233e3 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/specification.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -60,19 +60,19 @@
     bool -> local_theory -> (string * thm list) list * local_theory
   val theorem: string -> Method.text option ->
     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
-    Element.context_i list -> Element.statement_i ->
+    string list -> Element.context_i list -> Element.statement_i ->
     bool -> local_theory -> Proof.state
   val theorem_cmd: string -> Method.text option ->
     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
-    Element.context list -> Element.statement ->
+    (xstring * Position.T) list -> Element.context list -> Element.statement ->
     bool -> local_theory -> Proof.state
   val schematic_theorem: string -> Method.text option ->
     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
-    Element.context_i list -> Element.statement_i ->
+    string list -> Element.context_i list -> Element.statement_i ->
     bool -> local_theory -> Proof.state
   val schematic_theorem_cmd: string -> Method.text option ->
     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
-    Element.context list -> Element.statement ->
+    (xstring * Position.T) list -> Element.context list -> Element.statement ->
     bool -> local_theory -> Proof.state
   val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
 end;
@@ -378,16 +378,18 @@
   fun merge data : T = Library.merge (eq_snd op =) data;
 );
 
-fun gen_theorem schematic prep_att prep_stmt
-    kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy =
+fun gen_theorem schematic prep_bundle prep_att prep_stmt
+    kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
   let
-    val _ = Local_Theory.affirm lthy;
+    val _ = Local_Theory.assert lthy;
     val thy = Proof_Context.theory_of lthy;
 
     val attrib = prep_att thy;
+
     val elems = raw_elems |> map (Element.map_ctxt_attrib attrib);
-    val ((more_atts, prems, stmt, facts), goal_ctxt) =
-      prep_statement attrib prep_stmt elems raw_concl lthy;
+    val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy
+      |> Bundle.includes (map (prep_bundle lthy) raw_includes)
+      |> prep_statement attrib prep_stmt elems raw_concl;
     val atts = more_atts @ map attrib raw_atts;
 
     fun after_qed' results goal_ctxt' =
@@ -421,12 +423,13 @@
 
 in
 
-val theorem' = gen_theorem false (K I) Expression.cert_statement;
-fun theorem a b c d e f = theorem' a b c d e f;
-val theorem_cmd = gen_theorem false Attrib.intern_src Expression.read_statement;
+val theorem = gen_theorem false (K I) (K I) Expression.cert_statement;
+val theorem_cmd =
+  gen_theorem false Bundle.check Attrib.intern_src Expression.read_statement;
 
-val schematic_theorem = gen_theorem true (K I) Expression.cert_statement;
-val schematic_theorem_cmd = gen_theorem true Attrib.intern_src Expression.read_statement;
+val schematic_theorem = gen_theorem true (K I) (K I) Expression.cert_statement;
+val schematic_theorem_cmd =
+  gen_theorem true Bundle.check Attrib.intern_src Expression.read_statement;
 
 fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ()));
 
diff -r f4838ce57772 -r 3031603233e3 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -58,6 +58,8 @@
   val theory': (bool -> theory -> theory) -> transition -> transition
   val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
   val end_local_theory: transition -> transition
+  val open_target: (generic_theory -> local_theory) -> transition -> transition
+  val close_target: transition -> transition
   val local_theory': (xstring * Position.T) option -> (bool -> local_theory -> local_theory) ->
     transition -> transition
   val local_theory: (xstring * Position.T) option -> (local_theory -> local_theory) ->
@@ -105,7 +107,7 @@
 (* local theory wrappers *)
 
 val loc_init = Named_Target.context_cmd;
-val loc_exit = Local_Theory.exit_global;
+val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
 
 fun loc_begin loc (Context.Theory thy) = loc_init (the_default ("-", Position.none) loc) thy
   | loc_begin NONE (Context.Proof lthy) = lthy
@@ -456,6 +458,20 @@
   (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy)
     | _ => raise UNDEF));
 
+fun open_target f = transaction (fn _ =>
+  (fn Theory (gthy, _) =>
+        let val lthy = f gthy
+        in Theory (Context.Proof lthy, SOME lthy) end
+    | _ => raise UNDEF));
+
+val close_target = transaction (fn _ =>
+  (fn Theory (Context.Proof lthy, _) =>
+        (case try Local_Theory.close_target lthy of
+          SOME lthy' => Theory (Context.Proof lthy', SOME lthy)
+        | NONE => raise UNDEF)
+    | _ => raise UNDEF));
+
+
 local
 
 fun local_theory_presentation loc f = present_transaction (fn int =>
diff -r f4838ce57772 -r 3031603233e3 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Syntax/parser.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -201,7 +201,7 @@
                             val tk_prods =
                               these
                                 (AList.lookup (op =) nt_prods
-                                  (SOME (hd l_starts handle Empty => unknown_start)));
+                                  (SOME (hd l_starts handle List.Empty => unknown_start)));
 
                             (*add_lambda is true if an existing production of the nt
                               produces lambda due to the new lambda NT l*)
diff -r f4838ce57772 -r 3031603233e3 src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/library.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -328,7 +328,7 @@
 fun single x = [x];
 
 fun the_single [x] = x
-  | the_single _ = raise Empty;
+  | the_single _ = raise List.Empty;
 
 fun singleton f x = the_single (f [x]);
 
@@ -372,12 +372,12 @@
 
 (*  (op @) [x1, ..., xn]  ===>  ((x1 @ x2) @ x3) ... @ xn
     for operators that associate to the left (TAIL RECURSIVE)*)
-fun foldl1 f [] = raise Empty
+fun foldl1 f [] = raise List.Empty
   | foldl1 f (x :: xs) = foldl f (x, xs);
 
 (*  (op @) [x1, ..., xn]  ===>   x1 @ (x2 ... @ (x[n-1] @ xn))
     for n > 0, operators that associate to the right (not tail recursive)*)
-fun foldr1 f [] = raise Empty
+fun foldr1 f [] = raise List.Empty
   | foldr1 f l =
       let fun itr [x] = x
             | itr (x::l) = f(x, itr l)
@@ -454,7 +454,7 @@
   in mapp 0 end;
 
 (*rear decomposition*)
-fun split_last [] = raise Empty
+fun split_last [] = raise List.Empty
   | split_last [x] = ([], x)
   | split_last (x :: xs) = apfst (cons x) (split_last xs);
 
diff -r f4838ce57772 -r 3031603233e3 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Tools/induct.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -104,12 +104,12 @@
 
 val mk_var = Net.encode_type o #2 o Term.dest_Var;
 
-fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
+fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle List.Empty =>
   raise THM ("No variables in conclusion of rule", 0, [thm]);
 
 in
 
-fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
+fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle List.Empty =>
   raise THM ("No variables in major premise of rule", 0, [thm]);
 
 val left_var_concl = concl_var hd;
diff -r f4838ce57772 -r 3031603233e3 src/Tools/jEdit/etc/settings
--- a/src/Tools/jEdit/etc/settings	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Tools/jEdit/etc/settings	Wed Mar 21 23:41:22 2012 +0100
@@ -6,7 +6,7 @@
 JEDIT_OPTIONS="-reuseview -noserver -nobackground -log=9"
 JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss4m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
 #JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
-JEDIT_SYSTEM_OPTIONS="-Dapple.laf.useScreenMenuBar=true -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit"
+JEDIT_SYSTEM_OPTIONS="-Dapple.laf.useScreenMenuBar=false -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit"
 
 JEDIT_STYLE_SHEETS="$ISABELLE_HOME/etc/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css"
 
diff -r f4838ce57772 -r 3031603233e3 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Tools/subtyping.ML	Wed Mar 21 23:41:22 2012 +0100
@@ -832,7 +832,7 @@
       "\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi).";
 
     val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t))
-      handle Empty => error ("Not a proper map function:" ^ err_str t);
+      handle List.Empty => error ("Not a proper map function:" ^ err_str t);
 
     fun gen_arg_var ([], []) = []
       | gen_arg_var ((T, T') :: Ts, (U, U') :: Us) =