# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1465575134 -3600
# Node ID 06b021ff892023ea6b010fc04705a20f8d4ea7b9
# Parent  d2d26ff708d7f9d2b58fbf35273687cc32cc5af0# Parent  243fdbbbd4ef986208726b61ace6736498bde0db
Merge

diff -r d2d26ff708d7 -r 06b021ff8920 NEWS
--- a/NEWS	Fri Jun 10 15:53:08 2016 +0100
+++ b/NEWS	Fri Jun 10 17:12:14 2016 +0100
@@ -35,6 +35,16 @@
 * Old 'header' command is no longer supported (legacy since
 Isabelle2015).
 
+* Command 'bundle' provides a local theory target to define a bundle
+from the body of specification commands (such as 'declare',
+'declaration', 'notation', 'lemmas', 'lemma'). For example:
+
+bundle foo
+begin
+  declare a [simp]
+  declare b [intro]
+end
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
diff -r d2d26ff708d7 -r 06b021ff8920 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Fri Jun 10 15:53:08 2016 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Fri Jun 10 17:12:14 2016 +0100
@@ -206,6 +206,7 @@
 text \<open>
   \begin{matharray}{rcl}
     @{command_def "bundle"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+    @{command "bundle"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
     @{command_def "print_bundles"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
     @{command_def "include"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     @{command_def "including"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
@@ -226,7 +227,8 @@
   (\secref{sec:locale}).
 
   @{rail \<open>
-    @@{command bundle} @{syntax name} '=' @{syntax thms} @{syntax for_fixes}
+    @@{command bundle} @{syntax name}
+      ( '=' @{syntax thms} @{syntax for_fixes} | @'begin')
     ;
     @@{command print_bundles} ('!'?)
     ;
@@ -241,6 +243,13 @@
   morphisms, when moved into different application contexts; this works
   analogously to any other local theory specification.
 
+  \<^descr> \<^theory_text>\<open>bundle b begin body end\<close> defines a bundle of declarations from the
+  \<open>body\<close> of local theory specifications. It may consist of commands that are
+  technically equivalent to \<^theory_text>\<open>declare\<close> or \<^theory_text>\<open>declaration\<close>, which also includes
+  \<^theory_text>\<open>notation\<close>, for example. Named fact declarations like ``\<^theory_text>\<open>lemmas a [simp] =
+  b\<close>'' or ``\<^theory_text>\<open>lemma a [simp]: B \<proof>\<close>'' are also admitted, but the name
+  bindings are not recorded in the bundle.
+
   \<^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.
 
diff -r d2d26ff708d7 -r 06b021ff8920 src/HOL/Library/FinFun.thy
--- a/src/HOL/Library/FinFun.thy	Fri Jun 10 15:53:08 2016 +0100
+++ b/src/HOL/Library/FinFun.thy	Fri Jun 10 17:12:14 2016 +0100
@@ -189,12 +189,19 @@
   thus "curry f a \<in> finfun" unfolding finfun_def by auto
 qed
 
-bundle finfun =
-  fst_finfun[simp] snd_finfun[simp] Abs_finfun_inverse[simp] 
-  finfun_apply_inverse[simp] Abs_finfun_inject[simp] finfun_apply_inject[simp]
-  Diag_finfun[simp] finfun_curry[simp]
-  const_finfun[iff] fun_upd_finfun[iff] finfun_apply[iff] map_of_finfun[iff]
-  finfun_left_compose[intro] fst_finfun[intro] snd_finfun[intro]
+bundle finfun
+begin
+
+lemmas [simp] =
+  fst_finfun snd_finfun Abs_finfun_inverse
+  finfun_apply_inverse Abs_finfun_inject finfun_apply_inject
+  Diag_finfun finfun_curry
+lemmas [iff] =
+  const_finfun fun_upd_finfun finfun_apply map_of_finfun
+lemmas [intro] =
+  finfun_left_compose fst_finfun snd_finfun
+
+end
 
 lemma Abs_finfun_inject_finite:
   fixes x y :: "'a \<Rightarrow> 'b"
@@ -730,8 +737,8 @@
   "finite (UNIV :: 'a set) \<Longrightarrow> Finite_Set.fold (\<lambda>a. upd a b') (cnst b) (UNIV :: 'a set) = cnst b'"
 begin
 
-lemma finfun_rec_const [simp]: includes finfun shows
-  "finfun_rec cnst upd (K$ c) = cnst c"
+lemma finfun_rec_const [simp]: "finfun_rec cnst upd (K$ c) = cnst c"
+  including finfun
 proof(cases "finite (UNIV :: 'a set)")
   case False
   hence "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = c" by(simp add: finfun_default_const)
@@ -980,9 +987,9 @@
 by(simp add: finfun_comp2_def finfun_const_def comp_def)
 
 lemma finfun_comp2_update:
-  includes finfun
   assumes inj: "inj f"
   shows "finfun_comp2 (g(b $:= c)) f = (if b \<in> range f then (finfun_comp2 g f)(inv f b $:= c) else finfun_comp2 g f)"
+  including finfun
 proof(cases "b \<in> range f")
   case True
   from inj have "\<And>x. (op $ g)(f x := c) \<circ> f = (op $ g \<circ> f)(x := c)" by(auto intro!: ext dest: injD)
diff -r d2d26ff708d7 -r 06b021ff8920 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Jun 10 15:53:08 2016 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Jun 10 17:12:14 2016 +0100
@@ -33,11 +33,12 @@
   val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
     (('c * 'a list) * ('b * 'a list) list) list ->
     (('c * 'att list) * ('fact * 'att list) list) list
-  val global_notes: string -> (binding * (thm list * Token.src list) list) list ->
+  type thms = (thm list * Token.src list) list
+  val global_notes: string -> (binding * thms) list ->
     theory -> (string * thm list) list * theory
-  val local_notes: string -> (binding * (thm list * Token.src list) list) list ->
+  val local_notes: string -> (binding * thms) list ->
     Proof.context -> (string * thm list) list * Proof.context
-  val generic_notes: string -> (binding * (thm list * Token.src list) list) list ->
+  val generic_notes: string -> (binding * thms) list ->
     Context.generic -> (string * thm list) list * Context.generic
   val eval_thms: Proof.context -> (Facts.ref * Token.src list) list -> thm list
   val attribute_syntax: attribute context_parser -> Token.src -> attribute
@@ -47,16 +48,13 @@
   val attribute_setup: bstring * Position.T -> Input.source -> string ->
     local_theory -> local_theory
   val internal: (morphism -> attribute) -> Token.src
+  val internal_declaration: declaration -> thms
   val add_del: attribute -> attribute -> attribute context_parser
   val thm: thm context_parser
   val thms: thm list context_parser
   val multi_thm: thm list context_parser
-  val transform_facts: morphism ->
-    (Attrib.binding * (thm list * Token.src list) list) list ->
-    (Attrib.binding * (thm list * Token.src list) list) list
-  val partial_evaluation: Proof.context ->
-    (binding * (thm list * Token.src list) list) list ->
-    (binding * (thm list * Token.src list) list) list
+  val transform_facts: morphism -> (Attrib.binding * thms) list -> (Attrib.binding * thms) list
+  val partial_evaluation: Proof.context -> (binding * thms) list -> (binding * thms) list
   val print_options: bool -> Proof.context -> unit
   val config_bool: Binding.binding ->
     (Context.generic -> bool) -> bool Config.T * (theory -> theory)
@@ -194,6 +192,8 @@
 
 (* fact expressions *)
 
+type thms = (thm list * Token.src list) list;
+
 fun global_notes kind facts thy = thy |>
   Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts);
 
@@ -243,6 +243,9 @@
   internal_attribute_name ::
     [Token.make_string ("<attribute>", Position.none) |> Token.assign (SOME (Token.Attribute att))];
 
+fun internal_declaration decl =
+  [([Drule.dummy_thm], [internal (fn phi => Thm.declaration_attribute (K (decl phi)))])];
+
 
 (* add/del syntax *)
 
diff -r d2d26ff708d7 -r 06b021ff8920 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Fri Jun 10 15:53:08 2016 +0100
+++ b/src/Pure/Isar/bundle.ML	Fri Jun 10 17:12:14 2016 +0100
@@ -6,14 +6,15 @@
 
 signature BUNDLE =
 sig
-  type bundle = (thm list * Token.src list) list
   val check: Proof.context -> xstring * Position.T -> string
-  val get_bundle: Proof.context -> string -> bundle
-  val get_bundle_cmd: Proof.context -> xstring * Position.T -> bundle
-  val bundle: binding * (thm list * Token.src list) list ->
+  val get_bundle: Proof.context -> string -> Attrib.thms
+  val get_bundle_cmd: Proof.context -> xstring * Position.T -> Attrib.thms
+  val print_bundles: bool -> Proof.context -> unit
+  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 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
@@ -24,36 +25,82 @@
     generic_theory -> Binding.scope * local_theory
   val context_cmd: (xstring * Position.T) list -> Element.context list ->
     generic_theory -> Binding.scope * local_theory
-  val print_bundles: bool -> Proof.context -> unit
 end;
 
 structure Bundle: BUNDLE =
 struct
 
-(* maintain bundles *)
-
-type bundle = (thm list * Token.src list) list;
-
-fun transform_bundle phi : bundle -> bundle =
-  map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts));
+(** context data **)
 
 structure Data = Generic_Data
 (
-  type T = bundle Name_Space.table;
-  val empty : T = Name_Space.empty_table "bundle";
+  type T = Attrib.thms Name_Space.table * Attrib.thms option;
+  val empty : T = (Name_Space.empty_table "bundle", NONE);
   val extend = I;
-  val merge = Name_Space.merge_tables;
+  fun merge ((tab1, target1), (tab2, target2)) =
+    (Name_Space.merge_tables (tab1, tab2), merge_options (target1, target2));
 );
 
-val get_bundles = Data.get o Context.Proof;
+
+(* bundles *)
+
+val get_bundles_generic = #1 o Data.get;
+val get_bundles = get_bundles_generic o Context.Proof;
 
 fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
 
-val get_bundle = Name_Space.get o get_bundles;
+val get_bundle_generic = Name_Space.get o get_bundles_generic;
+val get_bundle = get_bundle_generic o Context.Proof;
 fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt;
 
+fun define_bundle def context =
+  let
+    val (name, bundles') = Name_Space.define context true def (get_bundles_generic context);
+    val context' = (Data.map o apfst o K) bundles' context;
+  in (name, context') end;
 
-(* define bundle *)
+
+(* target -- bundle under construction *)
+
+fun the_target thy =
+  (case #2 (Data.get (Context.Theory thy)) of
+    SOME thms => thms
+  | NONE => error "Missing bundle target");
+
+val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE;
+val set_target = Context.theory_map o Data.map o apsnd o K o SOME;
+
+fun augment_target thms =
+  Local_Theory.background_theory (fn thy => set_target (the_target thy @ thms) thy);
+
+
+(* print bundles *)
+
+fun pretty_bundle ctxt (markup_name, bundle) =
+  let
+    val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
+    fun prt_thm_attribs atts th =
+      Pretty.block (Pretty.breaks (prt_thm th :: Attrib.pretty_attribs ctxt atts));
+    fun prt_thms (ths, []) = map prt_thm ths
+      | prt_thms (ths, atts) = map (prt_thm_attribs atts) ths;
+  in
+    Pretty.block ([Pretty.keyword1 "bundle", Pretty.str " ", Pretty.mark_str markup_name] @
+      (if null bundle then [] else Pretty.fbreaks (Pretty.str " =" :: maps prt_thms bundle)))
+  end;
+
+fun print_bundles verbose ctxt =
+  Pretty.writeln_chunks
+    (map (pretty_bundle ctxt) (Name_Space.markup_table verbose ctxt (get_bundles ctxt)));
+
+
+
+(** define bundle **)
+
+fun transform_bundle phi =
+  map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts));
+
+
+(* command *)
 
 local
 
@@ -67,10 +114,7 @@
       |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
   in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
-      (fn phi => fn context =>
-        context |> Data.map
-          (#2 o Name_Space.define context true
-            (Morphism.binding phi binding, transform_bundle phi bundle)))
+      (fn phi => #2 o define_bundle (Morphism.binding phi binding, transform_bundle phi bundle))
   end;
 
 in
@@ -81,7 +125,72 @@
 end;
 
 
-(* include bundles *)
+(* target *)
+
+local
+
+fun bad_operation _ = error "Not possible in bundle target";
+
+fun conclude invisible binding =
+  Local_Theory.background_theory_result (fn thy =>
+    thy
+    |> invisible ? Context_Position.set_visible_global false
+    |> Context.Theory
+    |> define_bundle (binding, the_target thy)
+    ||> (Context.the_theory
+      #> invisible ? Context_Position.restore_visible_global thy
+      #> reset_target));
+
+fun pretty binding lthy =
+  let
+    val bundle = the_target (Proof_Context.theory_of lthy);
+    val (name, lthy') = lthy
+      |> Local_Theory.raw_theory (Context_Position.set_visible_global false)
+      |> conclude true binding;
+    val thy_ctxt' = Proof_Context.init_global (Proof_Context.theory_of lthy');
+    val markup_name =
+      Name_Space.markup_extern thy_ctxt' (Name_Space.space_of_table (get_bundles thy_ctxt')) name;
+  in [pretty_bundle lthy' (markup_name, bundle)] end;
+
+fun bundle_notes kind facts lthy =
+  let
+    val bundle = facts
+      |> maps (fn ((_, more_atts), thms) => map (fn (ths, atts) => (ths, atts @ more_atts)) thms);
+  in
+    lthy
+    |> augment_target (transform_bundle (Local_Theory.standard_morphism_theory lthy) bundle)
+    |> Generic_Target.standard_notes (op <>) kind facts
+    |> Attrib.local_notes kind facts
+  end;
+
+fun bundle_declaration decl lthy =
+  lthy
+  |> (augment_target o Attrib.internal_declaration)
+    (Morphism.transform (Local_Theory.standard_morphism_theory lthy) decl)
+  |> Generic_Target.standard_declaration (K true) decl;
+
+in
+
+fun init binding thy =
+  thy
+  |> Sign.change_begin
+  |> set_target []
+  |> Proof_Context.init_global
+  |> Local_Theory.init (Sign.naming_of thy)
+     {define = bad_operation,
+      notes = bundle_notes,
+      abbrev = bad_operation,
+      declaration = K bundle_declaration,
+      theory_registration = bad_operation,
+      locale_dependency = bad_operation,
+      pretty = pretty binding,
+      exit = conclude false binding #> #2 #> Local_Theory.target_of #> Sign.change_end_local}
+
+end;
+
+
+
+(** include bundles **)
 
 local
 
@@ -123,22 +232,4 @@
 
 end;
 
-
-(* print_bundles *)
-
-fun print_bundles verbose ctxt =
-  let
-    val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
-
-    fun prt_fact (ths, []) = map prt_thm ths
-      | prt_fact (ths, atts) = Pretty.enclose "(" ")"
-          (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
-
-    fun prt_bundle (name, bundle) =
-      Pretty.block (Pretty.keyword1 "bundle" :: Pretty.str " " :: Pretty.mark_str name ::
-        Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
-  in
-    map prt_bundle (Name_Space.markup_table verbose ctxt (get_bundles ctxt))
-  end |> Pretty.writeln_chunks;
-
 end;
diff -r d2d26ff708d7 -r 06b021ff8920 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Fri Jun 10 15:53:08 2016 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Fri Jun 10 17:12:14 2016 +0100
@@ -348,9 +348,10 @@
   let
     val thy = Proof_Context.theory_of lthy;
     val proto_sup = prep_class thy raw_sup;
-    val proto_sub = case Named_Target.class_of lthy of
+    val proto_sub =
+      (case Named_Target.class_of lthy of
         SOME class => class
-      | NONE => error "Not in a class target";
+      | NONE => error "Not in a class target");
     val (sub, sup) = Axclass.cert_classrel thy (proto_sub, proto_sup);
 
     val expr = ([(sup, (("", false), Expression.Positional []))], []);
diff -r d2d26ff708d7 -r 06b021ff8920 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Fri Jun 10 15:53:08 2016 +0100
+++ b/src/Pure/Isar/generic_target.ML	Fri Jun 10 17:12:14 2016 +0100
@@ -20,6 +20,12 @@
   val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
 
   (*nested local theories primitives*)
+  val standard_facts: local_theory -> Proof.context ->
+    (Attrib.binding * Attrib.thms) list -> (Attrib.binding * Attrib.thms) list
+  val standard_notes: (int * int -> bool) -> string -> (Attrib.binding * Attrib.thms) list ->
+    local_theory -> local_theory
+  val standard_declaration: (int * int -> bool) ->
+    (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
   val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
 
@@ -29,9 +35,9 @@
     bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val notes:
-    (string -> (Attrib.binding * (thm list * Token.src list) list) list ->
-      (Attrib.binding * (thm list * Token.src list) list) list -> local_theory -> local_theory) ->
-    string -> (Attrib.binding * (thm list * Token.src list) list) list -> local_theory ->
+    (string -> (Attrib.binding * Attrib.thms) list ->
+      (Attrib.binding * Attrib.thms) list -> local_theory -> local_theory) ->
+    string -> (Attrib.binding * Attrib.thms) list -> local_theory ->
     (string * thm list) list * local_theory
   val abbrev: (Syntax.mode -> binding * mixfix -> term ->
       term list * term list -> local_theory -> local_theory) ->
@@ -40,10 +46,8 @@
   (*theory target primitives*)
   val theory_target_foundation: ((binding * typ) * mixfix) * (binding * term) ->
      term list * term list -> local_theory -> (term * thm) * local_theory
-  val theory_target_notes: string ->
-    (Attrib.binding * (thm list * Token.src list) list) list ->
-    (Attrib.binding * (thm list * Token.src list) list) list ->
-    local_theory -> local_theory
+  val theory_target_notes: string -> (Attrib.binding * Attrib.thms) list ->
+    (Attrib.binding * Attrib.thms) list -> local_theory -> local_theory
   val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
     local_theory -> local_theory
 
@@ -55,10 +59,8 @@
     local_theory -> local_theory
 
   (*locale target primitives*)
-  val locale_target_notes: string -> string ->
-    (Attrib.binding * (thm list * Token.src list) list) list ->
-    (Attrib.binding * (thm list * Token.src list) list) list ->
-    local_theory -> local_theory
+  val locale_target_notes: string -> string -> (Attrib.binding * Attrib.thms) list ->
+    (Attrib.binding * Attrib.thms) list -> local_theory -> local_theory
   val locale_target_abbrev: string -> Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
     local_theory -> local_theory
   val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
diff -r d2d26ff708d7 -r 06b021ff8920 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Fri Jun 10 15:53:08 2016 +0100
+++ b/src/Pure/Isar/local_theory.ML	Fri Jun 10 17:12:14 2016 +0100
@@ -10,6 +10,7 @@
 structure Attrib =
 struct
   type binding = binding * Token.src list;
+  type thms = (thm list * Token.src list) list;
 end;
 
 signature LOCAL_THEORY =
@@ -30,6 +31,7 @@
   val new_group: local_theory -> local_theory
   val reset_group: local_theory -> local_theory
   val standard_morphism: local_theory -> Proof.context -> morphism
+  val standard_morphism_theory: local_theory -> morphism
   val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
@@ -45,10 +47,10 @@
   val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
-  val notes: (Attrib.binding * (thm list * Token.src list) list) list ->
-    local_theory -> (string * thm list) list * local_theory
-  val notes_kind: string -> (Attrib.binding * (thm list * Token.src list) list) list ->
-    local_theory -> (string * thm list) list * local_theory
+  val notes: (Attrib.binding * Attrib.thms) list -> local_theory ->
+    (string * thm list) list * local_theory
+  val notes_kind: string -> (Attrib.binding * Attrib.thms) list -> local_theory ->
+    (string * thm list) list * local_theory
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
   val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
@@ -85,9 +87,8 @@
 type operations =
  {define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory,
-  notes: string ->
-    (Attrib.binding * (thm list * Token.src list) list) list ->
-    local_theory -> (string * thm list) list * local_theory,
+  notes: string -> (Attrib.binding * Attrib.thms) list -> local_theory ->
+    (string * thm list) list * local_theory,
   abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory,
   declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
@@ -195,6 +196,9 @@
   Morphism.binding_morphism "Local_Theory.standard_binding"
     (Name_Space.transform_binding (Proof_Context.naming_of lthy));
 
+fun standard_morphism_theory lthy =
+  standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
+
 fun standard_form lthy ctxt x =
   Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
 
diff -r d2d26ff708d7 -r 06b021ff8920 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Jun 10 15:53:08 2016 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Jun 10 17:12:14 2016 +0100
@@ -35,7 +35,7 @@
     thm option * thm option -> thm list ->
     Element.context_i list ->
     declaration list ->
-    (string * (Attrib.binding * (thm list * Token.src list) list) list) list ->
+    (string * (Attrib.binding * Attrib.thms) list) list ->
     (string * morphism) list -> theory -> theory
   val intern: theory -> xstring -> string
   val check: theory -> xstring * Position.T -> string
@@ -50,7 +50,7 @@
   val specification_of: theory -> string -> term option * term list
 
   (* Storing results *)
-  val add_thmss: string -> string -> (Attrib.binding * (thm list * Token.src list) list) list ->
+  val add_thmss: string -> string -> (Attrib.binding * Attrib.thms) list ->
     Proof.context -> Proof.context
   val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
 
@@ -135,7 +135,7 @@
   (*syntax declarations*)
   syntax_decls: (declaration * serial) list,
   (*theorem declarations*)
-  notes: ((string * (Attrib.binding * (thm list * Token.src list) list) list) * serial) list,
+  notes: ((string * (Attrib.binding * Attrib.thms) list) * serial) list,
   (*locale dependencies (sublocale relation) in reverse order*)
   dependencies: ((string * (morphism * morphism)) * serial) list,
   (*mixin part of dependencies*)
@@ -612,21 +612,10 @@
 
 (* Declarations *)
 
-local
-
-fun add_decl loc decl =
-  add_thmss loc ""
-    [((Binding.empty, [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
-      [([Drule.dummy_thm], [])])];
-
-in
-
 fun add_declaration loc syntax decl =
   syntax ?
     Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
-  #> add_decl loc decl;
-
-end;
+  #> add_thmss loc "" [(Attrib.empty_binding, Attrib.internal_declaration decl)];
 
 
 (*** Reasoning about locales ***)
diff -r d2d26ff708d7 -r 06b021ff8920 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Fri Jun 10 15:53:08 2016 +0100
+++ b/src/Pure/Isar/named_target.ML	Fri Jun 10 17:12:14 2016 +0100
@@ -40,14 +40,14 @@
   else NONE;
 
 fun is_theory lthy =
-  case get_data lthy of
+  (case get_data lthy of
     SOME ("", _) => true
-  | _ => false;
+  | _ => false);
 
 fun target_of lthy =
-  case get_data lthy of
+  (case get_data lthy of
     NONE => error "Not in a named target"
-  | SOME (target, _) => target;
+  | SOME (target, _) => target);
 
 fun locale_name_of NONE = NONE
   | locale_name_of (SOME ("", _)) = NONE
@@ -58,9 +58,9 @@
 val bottom_locale_of = locale_name_of o get_bottom_data;
 
 fun class_of lthy =
-  case get_data lthy of
+  (case get_data lthy of
     SOME (class, true) => SOME class
-  | _ => NONE;
+  | _ => NONE);
 
 
 (* operations *)
diff -r d2d26ff708d7 -r 06b021ff8920 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Jun 10 15:53:08 2016 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Jun 10 17:12:14 2016 +0100
@@ -11,6 +11,8 @@
   type command_keyword = string * Position.T
   val command: command_keyword -> string ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
+  val maybe_begin_local_theory: command_keyword -> string ->
+    (local_theory -> local_theory) parser -> (theory -> local_theory) parser -> unit
   val local_theory': command_keyword -> string ->
     (bool -> local_theory -> local_theory) parser -> unit
   val local_theory: command_keyword -> string ->
@@ -25,7 +27,7 @@
   val parse_spans: Token.T list -> Command_Span.span list
   val side_comments: Token.T list -> Token.T list
   val command_reports: theory -> Token.T -> Position.report_text list
-  val check_command: Proof.context -> string * Position.T -> string
+  val check_command: Proof.context -> command_keyword -> string
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =
@@ -148,6 +150,14 @@
 fun command (name, pos) comment parse =
   raw_command (name, pos) comment (Parser parse);
 
+fun maybe_begin_local_theory command_keyword comment parse_local parse_global =
+  raw_command command_keyword comment
+    (Restricted_Parser (fn restricted =>
+      Parse.opt_target -- parse_local
+        >> (fn (target, f) => Toplevel.local_theory restricted target f) ||
+      (if is_some restricted then Scan.fail
+       else parse_global >> Toplevel.begin_local_theory true)));
+
 fun local_theory_command trans command_keyword comment parse =
   raw_command command_keyword comment
     (Restricted_Parser (fn restricted =>
diff -r d2d26ff708d7 -r 06b021ff8920 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Jun 10 15:53:08 2016 +0100
+++ b/src/Pure/Isar/specification.ML	Fri Jun 10 17:12:14 2016 +0100
@@ -51,7 +51,7 @@
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   val theorems: string ->
-    (Attrib.binding * (thm list * Token.src list) list) list ->
+    (Attrib.binding * Attrib.thms) list ->
     (binding * typ option * mixfix) list ->
     bool -> local_theory -> (string * thm list) list * local_theory
   val theorems_cmd: string ->
diff -r d2d26ff708d7 -r 06b021ff8920 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri Jun 10 15:53:08 2016 +0100
+++ b/src/Pure/Pure.thy	Fri Jun 10 17:12:14 2016 +0100
@@ -31,7 +31,7 @@
     "declaration" "syntax_declaration"
     "parse_ast_translation" "parse_translation" "print_translation"
     "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
-  and "bundle" :: thy_decl
+  and "bundle" :: thy_decl_block
   and "include" "including" :: prf_decl
   and "print_bundles" :: diag
   and "context" "locale" "experiment" :: thy_decl_block
@@ -491,9 +491,11 @@
 local
 
 val _ =
-  Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations"
+  Outer_Syntax.maybe_begin_local_theory @{command_keyword bundle}
+    "define bundle of declarations"
     ((Parse.binding --| @{keyword "="}) -- Parse.thms1 -- Parse.for_fixes
-      >> (uncurry Bundle.bundle_cmd));
+      >> (uncurry Bundle.bundle_cmd))
+    (Parse.binding --| Parse.begin >> Bundle.init);
 
 val _ =
   Outer_Syntax.command @{command_keyword include}