equal
deleted
inserted
replaced
11 sig |
11 sig |
12 type operations |
12 type operations |
13 val target_of: local_theory -> Proof.context |
13 val target_of: local_theory -> Proof.context |
14 val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory |
14 val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory |
15 val raw_theory: (theory -> theory) -> local_theory -> local_theory |
15 val raw_theory: (theory -> theory) -> local_theory -> local_theory |
|
16 val full_naming: local_theory -> NameSpace.naming |
16 val full_name: local_theory -> bstring -> string |
17 val full_name: local_theory -> bstring -> string |
17 val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory |
18 val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory |
18 val theory: (theory -> theory) -> local_theory -> local_theory |
19 val theory: (theory -> theory) -> local_theory -> local_theory |
19 val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory |
20 val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory |
20 val target: (Proof.context -> Proof.context) -> local_theory -> local_theory |
21 val target: (Proof.context -> Proof.context) -> local_theory -> local_theory |
120 |> ProofContext.transfer thy'; |
121 |> ProofContext.transfer thy'; |
121 in (res, lthy') end; |
122 in (res, lthy') end; |
122 |
123 |
123 fun raw_theory f = #2 o raw_theory_result (f #> pair ()); |
124 fun raw_theory f = #2 o raw_theory_result (f #> pair ()); |
124 |
125 |
125 fun full_name lthy = |
126 fun full_naming lthy = |
126 let |
127 Sign.naming_of (ProofContext.theory_of lthy) |
127 val naming = Sign.naming_of (ProofContext.theory_of lthy) |
128 |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy)) |
128 |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy)) |
129 |> NameSpace.qualified_names; |
129 |> NameSpace.qualified_names; |
130 |
130 in NameSpace.full naming end; |
131 val full_name = NameSpace.full o full_naming; |
131 |
132 |
132 fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy |
133 fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy |
133 |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy)) |
134 |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy)) |
134 |> Sign.qualified_names |
135 |> Sign.qualified_names |
135 |> f |
136 |> f |