# HG changeset patch
# User haftmann
# Date 1400773979 -7200
# Node ID c97b8250c033c2cd3490b6b0ec8dc88a82b9b495
# Parent  6a8a01e6dcdf9a8a97915dab005c6b428383dd2c
unused

diff -r 6a8a01e6dcdf -r c97b8250c033 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Thu May 22 16:59:49 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Thu May 22 17:52:59 2014 +0200
@@ -9,7 +9,6 @@
 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
@@ -48,15 +47,6 @@
 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 *)