# HG changeset patch
# User wenzelm
# Date 1465555534 -7200
# Node ID 302daf91896687367ebf5725284857ba2ac8ece6
# Parent  6d8a67a77bad7b5fc70bea5f845c75d78ce39fca
prefer hybrid 'bundle' command;

diff -r 6d8a67a77bad -r 302daf918966 NEWS
--- a/NEWS	Thu Jun 09 17:14:13 2016 +0200
+++ b/NEWS	Fri Jun 10 12:45:34 2016 +0200
@@ -35,9 +35,15 @@
 * Old 'header' command is no longer supported (legacy since
 Isabelle2015).
 
-* Command 'bundle_definition' provides a local theory target to define a
-bundle from the body of specification commands (e.g. 'declare',
-'declaration', 'notation', 'lemmas', 'lemma').
+* 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 6d8a67a77bad -r 302daf918966 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Thu Jun 09 17:14:13 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Fri Jun 10 12:45:34 2016 +0200
@@ -206,7 +206,7 @@
 text \<open>
   \begin{matharray}{rcl}
     @{command_def "bundle"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
-    @{command_def "bundle_definition"} & : & \<open>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> \\
@@ -227,9 +227,8 @@
   (\secref{sec:locale}).
 
   @{rail \<open>
-    @@{command bundle} @{syntax name} '=' @{syntax thms} @{syntax for_fixes}
-    ;
-    @@{command bundle_definition} @{syntax name} @'begin'
+    @@{command bundle} @{syntax name}
+      ( '=' @{syntax thms} @{syntax for_fixes} | @'begin')
     ;
     @@{command print_bundles} ('!'?)
     ;
@@ -244,12 +243,12 @@
   morphisms, when moved into different application contexts; this works
   analogously to any other local theory specification.
 
-  \<^descr> \<^theory_text>\<open>bundle_definition 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>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 6d8a67a77bad -r 302daf918966 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Jun 09 17:14:13 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Jun 10 12:45:34 2016 +0200
@@ -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 ->
@@ -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 6d8a67a77bad -r 302daf918966 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Jun 09 17:14:13 2016 +0200
+++ b/src/Pure/Pure.thy	Fri Jun 10 12:45:34 2016 +0200
@@ -31,8 +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_definition" :: thy_decl_block
+  and "bundle" :: thy_decl_block
   and "include" "including" :: prf_decl
   and "print_bundles" :: diag
   and "context" "locale" "experiment" :: thy_decl_block
@@ -492,14 +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));
-
-val _ =
-  Outer_Syntax.command @{command_keyword bundle_definition}
-    "define bundle of declarations (local theory target)"
-    (Parse.binding --| Parse.begin >> (Toplevel.begin_local_theory true o Bundle.init));
+      >> (uncurry Bundle.bundle_cmd))
+    (Parse.binding --| Parse.begin >> Bundle.init);
 
 val _ =
   Outer_Syntax.command @{command_keyword include}