--- a/src/Pure/Isar/named_target.ML Sat May 25 13:59:08 2013 +0200
+++ b/src/Pure/Isar/named_target.ML Sat May 25 15:44:08 2013 +0200
@@ -8,6 +8,8 @@
signature NAMED_TARGET =
sig
val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
+ val is_theory: local_theory -> bool
+ val the_name: local_theory -> string
val init: (local_theory -> local_theory) -> string -> theory -> local_theory
val theory_init: theory -> local_theory
val reinit: local_theory -> local_theory -> local_theory
@@ -43,6 +45,17 @@
Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
{target = target, is_locale = is_locale, is_class = is_class});
+fun is_theory lthy = Option.map #target (peek lthy) = SOME ""
+ andalso Local_Theory.level lthy = 1;
+
+fun the_name lthy =
+ let
+ val _ = Local_Theory.assert_bottom true lthy;
+ in case Option.map #target (peek lthy) of
+ SOME target => target
+ | _ => error "Not in a named target"
+ end;
+
(* consts in locale *)