src/Pure/Isar/named_target.ML

--- a/src/Pure/Isar/named_target.ML	Wed Mar 21 17:16:39 2012 +0100
+++ b/src/Pure/Isar/named_target.ML	Wed Mar 21 17:25:35 2012 +0100
@@ -2,16 +2,17 @@
     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 =
@@ -43,6 +44,10 @@
   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 *)
 
@@ -209,11 +214,9 @@
 
 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;