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}