--- a/src/Pure/Isar/local_theory.ML Wed Mar 11 15:45:40 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML Wed Mar 11 16:36:27 2009 +0100
@@ -138,14 +138,12 @@
fun full_naming lthy =
Sign.naming_of (ProofContext.theory_of lthy)
- |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy))
- |> NameSpace.qualified_names;
+ |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy));
fun full_name naming = NameSpace.full_name (full_naming naming);
fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
|> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))
- |> Sign.qualified_names
|> f
||> Sign.restore_naming thy);