# HG changeset patch
# User wenzelm
# Date 1170622940 -3600
# Node ID 36cc1875619ff745d4c7ea089f679a3edb99d02c
# Parent  9ddd3349d5973e61b55beb675afc4c9e0e665ae0
added full_naming;

diff -r 9ddd3349d597 -r 36cc1875619f src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sun Feb 04 22:02:19 2007 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sun Feb 04 22:02:20 2007 +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_naming: local_theory -> NameSpace.naming
   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
@@ -122,12 +123,12 @@
 
 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 full_naming lthy =
+  Sign.naming_of (ProofContext.theory_of lthy)
+  |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy))
+  |> NameSpace.qualified_names;
+
+val full_name = NameSpace.full o full_naming;
 
 fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
   |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))