
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}




