src/Pure/Isar/local_theory.ML
changeset 28991 694227dd3e8c
parent 28965 1de908189869
child 29134 9657871890c7
     1.1 --- a/src/Pure/Isar/local_theory.ML	Thu Dec 04 14:44:07 2008 +0100
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Fri Dec 05 08:04:53 2008 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4    val raw_theory: (theory -> theory) -> local_theory -> local_theory
     1.5    val checkpoint: local_theory -> local_theory
     1.6    val full_naming: local_theory -> NameSpace.naming
     1.7 -  val full_name: local_theory -> bstring -> string
     1.8 +  val full_name: local_theory -> Binding.T -> string
     1.9    val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
    1.10    val theory: (theory -> theory) -> local_theory -> local_theory
    1.11    val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
    1.12 @@ -142,7 +142,7 @@
    1.13    |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy))
    1.14    |> NameSpace.qualified_names;
    1.15  
    1.16 -fun full_name naming = NameSpace.full_name (full_naming naming) o Binding.name;
    1.17 +fun full_name naming = NameSpace.full_name (full_naming naming);
    1.18  
    1.19  fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
    1.20    |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))