# HG changeset patch
# User wenzelm
# Date 1333305739 -7200
# Node ID 13a770bd5544c04669ab9b6df99cf96bed98d4ce
# Parent  6523a21076a8071363e1d527fcc7f082574a08cd
nothing specific about named target;

diff -r 6523a21076a8 -r 13a770bd5544 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Sun Apr 01 20:36:33 2012 +0200
+++ b/src/Pure/Isar/bundle.ML	Sun Apr 01 20:42:19 2012 +0200
@@ -95,7 +95,7 @@
       |> Local_Theory.target (gen_includes prep args)
       |> Local_Theory.restore
   | gen_context prep args (Context.Proof lthy) =
-      Named_Target.assert lthy
+      Local_Theory.assert lthy
       |> gen_includes prep args
       |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
 
diff -r 6523a21076a8 -r 13a770bd5544 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sun Apr 01 20:36:33 2012 +0200
+++ b/src/Pure/Isar/named_target.ML	Sun Apr 01 20:42:19 2012 +0200
@@ -8,7 +8,6 @@
 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
@@ -44,10 +43,6 @@
   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)";
-
 
 (* consts in locale *)