--- a/src/Pure/Isar/locale.ML Mon Feb 19 14:30:06 2018 +0100
+++ b/src/Pure/Isar/locale.ML Mon Feb 19 14:49:11 2018 +0100
@@ -468,7 +468,7 @@
|> Context_Position.set_visible_generic false
|> pair (Idents.get context)
|> roundup (Context.theory_of context)
- (activate_notes Element.init' (Morphism.transfer_morphism o Context.theory_of) context export)
+ (activate_notes Element.init' Morphism.transfer_morphism'' context export)
(the_default Morphism.identity export) dep
|-> Idents.put
|> Context_Position.restore_visible_generic context;
@@ -481,7 +481,7 @@
context
|> Context_Position.set_visible_generic false
|> pair empty_idents
- |> activate_all name thy Element.init' (Morphism.transfer_morphism o Context.theory_of)
+ |> activate_all name thy Element.init' Morphism.transfer_morphism''
|-> (fn marked' => Idents.put (merge_idents (marked, marked')))
|> Context_Position.restore_visible_generic context
|> Context.proof_of