src/Pure/Isar/local_theory.ML
changeset 52119 90ba620333d0
parent 52118 2a976115c7c3
child 52140 88a69da5d3fa
     1.1 --- a/src/Pure/Isar/local_theory.ML	Wed May 22 22:56:17 2013 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Wed May 22 22:56:17 2013 +0200
     1.3 @@ -36,6 +36,7 @@
     1.4    val target_of: local_theory -> Proof.context
     1.5    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
     1.6    val target_morphism: local_theory -> morphism
     1.7 +  val surface_target: (Proof.context -> Proof.context) -> local_theory -> local_theory
     1.8    val propagate_ml_env: generic_theory -> generic_theory
     1.9    val operations_of: local_theory -> operations
    1.10    val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    1.11 @@ -231,6 +232,10 @@
    1.12  
    1.13  fun target_morphism lthy = standard_morphism lthy (target_of lthy);
    1.14  
    1.15 +fun surface_target f =
    1.16 +  map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
    1.17 +    (naming, operations, after_close, brittle, f target));
    1.18 +
    1.19  fun propagate_ml_env (context as Context.Proof lthy) =
    1.20        let val inherit = ML_Env.inherit context in
    1.21          lthy