equal
deleted
inserted
replaced
17 val target_of: local_theory -> Proof.context |
17 val target_of: local_theory -> Proof.context |
18 val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory |
18 val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory |
19 val raw_theory: (theory -> theory) -> local_theory -> local_theory |
19 val raw_theory: (theory -> theory) -> local_theory -> local_theory |
20 val checkpoint: local_theory -> local_theory |
20 val checkpoint: local_theory -> local_theory |
21 val full_naming: local_theory -> NameSpace.naming |
21 val full_naming: local_theory -> NameSpace.naming |
22 val full_name: local_theory -> bstring -> string |
22 val full_name: local_theory -> Binding.T -> string |
23 val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory |
23 val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory |
24 val theory: (theory -> theory) -> local_theory -> local_theory |
24 val theory: (theory -> theory) -> local_theory -> local_theory |
25 val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory |
25 val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory |
26 val target: (Proof.context -> Proof.context) -> local_theory -> local_theory |
26 val target: (Proof.context -> Proof.context) -> local_theory -> local_theory |
27 val affirm: local_theory -> local_theory |
27 val affirm: local_theory -> local_theory |
140 fun full_naming lthy = |
140 fun full_naming lthy = |
141 Sign.naming_of (ProofContext.theory_of lthy) |
141 Sign.naming_of (ProofContext.theory_of lthy) |
142 |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy)) |
142 |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy)) |
143 |> NameSpace.qualified_names; |
143 |> NameSpace.qualified_names; |
144 |
144 |
145 fun full_name naming = NameSpace.full_name (full_naming naming) o Binding.name; |
145 fun full_name naming = NameSpace.full_name (full_naming naming); |
146 |
146 |
147 fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy |
147 fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy |
148 |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy)) |
148 |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy)) |
149 |> Sign.qualified_names |
149 |> Sign.qualified_names |
150 |> f |
150 |> f |