# HG changeset patch
# User wenzelm
# Date 1465485232 -7200
# Node ID ecaa677d20bc47d5ab0595dc62366385ea397ad2
# Parent  7dd3ee7ee422087a282d03b33a359f35ac304daa
clarified;

diff -r 7dd3ee7ee422 -r ecaa677d20bc src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Jun 09 15:41:49 2016 +0200
+++ b/src/Pure/Pure.thy	Thu Jun 09 17:13:52 2016 +0200
@@ -32,7 +32,7 @@
     "parse_ast_translation" "parse_translation" "print_translation"
     "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
   and "bundle" :: thy_decl
-  and "bundle_target" :: thy_decl_block
+  and "bundle_definition" :: thy_decl_block
   and "include" "including" :: prf_decl
   and "print_bundles" :: diag
   and "context" "locale" "experiment" :: thy_decl_block
@@ -497,7 +497,8 @@
       >> (uncurry Bundle.bundle_cmd));
 
 val _ =
-  Outer_Syntax.command @{command_keyword bundle_target} "define bundle of declarations"
+  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));
 
 val _ =