src/Pure/Isar/locale.ML
changeset 54795 e58623a33ba5
parent 53171 a5e54d4d9081
child 55300 0594b429baf9
equal deleted inserted replaced
54794:e279c2ceb54c 54795:e58623a33ba5
   453     roundup thy activate (the_default Morphism.identity export) dep (Idents.get context, context)
   453     roundup thy activate (the_default Morphism.identity export) dep (Idents.get context, context)
   454     |-> Idents.put
   454     |-> Idents.put
   455   end;
   455   end;
   456 
   456 
   457 fun init name thy =
   457 fun init name thy =
   458   activate_all name thy Element.init (Morphism.transfer_morphism o Context.theory_of)
   458   let
   459     (empty_idents, Context.Proof (Proof_Context.init_global thy))
   459     val context = Context.Proof (Proof_Context.init_global thy);
   460   |-> Idents.put |> Context.proof_of;
   460     val marked = Idents.get context;
       
   461     val (marked', context') = activate_all name thy Element.init
       
   462       (Morphism.transfer_morphism o Context.theory_of) (empty_idents, context)
       
   463   in
       
   464     context'
       
   465     |> Idents.put (merge_idents (marked, marked'))
       
   466     |> Context.proof_of
       
   467   end;
   461 
   468 
   462 
   469 
   463 (*** Add and extend registrations ***)
   470 (*** Add and extend registrations ***)
   464 
   471 
   465 fun amend_registration (name, morph) mixin export context =
   472 fun amend_registration (name, morph) mixin export context =