src/Pure/Isar/local_theory.ML
changeset 30438 c2d49315b93b
parent 29581 b3b33e0298eb
child 30469 de9e8f1d927c
     1.1 --- a/src/Pure/Isar/local_theory.ML	Wed Mar 11 15:45:40 2009 +0100
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Mar 11 16:36:27 2009 +0100
     1.3 @@ -138,14 +138,12 @@
     1.4  
     1.5  fun full_naming lthy =
     1.6    Sign.naming_of (ProofContext.theory_of lthy)
     1.7 -  |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy))
     1.8 -  |> NameSpace.qualified_names;
     1.9 +  |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy));
    1.10  
    1.11  fun full_name naming = NameSpace.full_name (full_naming naming);
    1.12  
    1.13  fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
    1.14    |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))
    1.15 -  |> Sign.qualified_names
    1.16    |> f
    1.17    ||> Sign.restore_naming thy);
    1.18