src/Pure/Isar/named_target.ML

 (*  Title:      Pure/Isar/named_target.ML
     Author:     Makarius
     Author:     Florian Haftmann, TU Muenchen
 
-Targets for theory, locale and class.
+Targets for theory, locale, class -- at the bottom the nested structure.
 *)
 
 signature NAMED_TARGET =
 sig
+  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
+  val assert: local_theory -> local_theory
   val init: (local_theory -> local_theory) -> string -> theory -> local_theory
   val theory_init: theory -> local_theory
   val reinit: local_theory -> local_theory -> local_theory
   val context_cmd: xstring * Position.T -> theory -> local_theory
-  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
 end;
 
 structure Named_Target: NAMED_TARGET =
 struct
 

 );
 
 val peek =
   Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
     {target = target, is_locale = is_locale, is_class = is_class});
+
+fun assert lthy =
+  if is_some (peek lthy) then lthy
+  else error "Not in a named target (global theory, locale, class)";
 
 
 (* generic declarations *)
 
 fun locale_declaration locale syntax decl lthy =

         exit = Local_Theory.target_of o before_exit}
   end;
 
 val theory_init = init I "";
 
-fun reinit lthy =
-  (case Data.get lthy of
-    SOME (Target {target, before_exit, ...}) =>
-      init before_exit target o Local_Theory.exit_global
-  | NONE => error "Not in a named target");
+val reinit =
+  assert #> Data.get #> the #>
+  (fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target);
 
 fun context_cmd ("-", _) thy = init I "" thy
   | context_cmd target thy = init I (Locale.check thy target) thy;
 
 end;