diff -r ae3bb930b50f -r 89105c15b436 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Nov 30 16:48:42 2006 +0100
+++ b/src/Pure/Isar/local_theory.ML	Thu Nov 30 17:42:21 2006 +0100
@@ -13,6 +13,7 @@
   val target_of: local_theory -> Proof.context
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
+  val full_name: local_theory -> bstring -> string
   val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val theory: (theory -> theory) -> local_theory -> local_theory
   val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
@@ -118,6 +119,13 @@
 
 fun raw_theory f = #2 o raw_theory_result (f #> pair ());
 
+fun full_name lthy =
+  let
+    val naming = Sign.naming_of (ProofContext.theory_of lthy)
+      |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy))
+      |> NameSpace.qualified_names;
+  in NameSpace.full naming end;  
+
 fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
   |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))
   |> Sign.qualified_names