src/Pure/Isar/local_theory.ML
changeset 59887 43dc3c660f41
parent 59886 e0dc738eb08c
child 59890 01aff5aa081d
equal deleted inserted replaced
59886:e0dc738eb08c 59887:43dc3c660f41
   220   in (res, lthy') end;
   220   in (res, lthy') end;
   221 
   221 
   222 fun raw_theory f = #2 o raw_theory_result (f #> pair ());
   222 fun raw_theory f = #2 o raw_theory_result (f #> pair ());
   223 
   223 
   224 fun background_theory_result f lthy =
   224 fun background_theory_result f lthy =
   225   lthy |> raw_theory_result (fn thy =>
   225   let
   226     thy
   226     val naming =
   227     |> Sign.map_naming (K (background_naming_of lthy))
   227       background_naming_of lthy
   228     |> f
   228       |> Name_Space.transform_naming (Proof_Context.naming_of lthy);
   229     ||> Sign.restore_naming thy);
   229   in
       
   230     lthy |> raw_theory_result (fn thy =>
       
   231       thy
       
   232       |> Sign.map_naming (K naming)
       
   233       |> f
       
   234       ||> Sign.restore_naming thy)
       
   235   end;
   230 
   236 
   231 fun background_theory f = #2 o background_theory_result (f #> pair ());
   237 fun background_theory f = #2 o background_theory_result (f #> pair ());
   232 
   238 
   233 
   239 
   234 (* target contexts *)
   240 (* target contexts *)