src/Pure/Isar/locale.ML
changeset 55300 0594b429baf9
parent 54795 e58623a33ba5
child 55695 c05d3e22adaf
equal deleted inserted replaced
55281:765555d6a0b2 55300:0594b429baf9
   456 
   456 
   457 fun init name thy =
   457 fun init name thy =
   458   let
   458   let
   459     val context = Context.Proof (Proof_Context.init_global thy);
   459     val context = Context.Proof (Proof_Context.init_global thy);
   460     val marked = Idents.get context;
   460     val marked = Idents.get context;
   461     val (marked', context') = activate_all name thy Element.init
   461     val (marked', context') = (empty_idents, context)
   462       (Morphism.transfer_morphism o Context.theory_of) (empty_idents, context)
   462       |> activate_all name thy Element.init (Morphism.transfer_morphism o Context.theory_of);
   463   in
   463   in
   464     context'
   464     context'
   465     |> Idents.put (merge_idents (marked, marked'))
   465     |> Idents.put (merge_idents (marked, marked'))
   466     |> Context.proof_of
   466     |> Context.proof_of
   467   end;
   467   end;