src/Pure/Pure.thy
changeset 63271 ecaa677d20bc
parent 63270 7dd3ee7ee422
child 63273 302daf918966
     1.1 --- a/src/Pure/Pure.thy	Thu Jun 09 15:41:49 2016 +0200
     1.2 +++ b/src/Pure/Pure.thy	Thu Jun 09 17:13:52 2016 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4      "parse_ast_translation" "parse_translation" "print_translation"
     1.5      "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
     1.6    and "bundle" :: thy_decl
     1.7 -  and "bundle_target" :: thy_decl_block
     1.8 +  and "bundle_definition" :: thy_decl_block
     1.9    and "include" "including" :: prf_decl
    1.10    and "print_bundles" :: diag
    1.11    and "context" "locale" "experiment" :: thy_decl_block
    1.12 @@ -497,7 +497,8 @@
    1.13        >> (uncurry Bundle.bundle_cmd));
    1.14  
    1.15  val _ =
    1.16 -  Outer_Syntax.command @{command_keyword bundle_target} "define bundle of declarations"
    1.17 +  Outer_Syntax.command @{command_keyword bundle_definition}
    1.18 +    "define bundle of declarations (local theory target)"
    1.19      (Parse.binding --| Parse.begin >> (Toplevel.begin_local_theory true o Bundle.init));
    1.20  
    1.21  val _ =