tuned;
authorwenzelm
Mon, 03 Feb 2014 13:45:54 +0100
changeset 55300 0594b429baf9
parent 55281 765555d6a0b2
child 55301 792f3cf59d95
tuned;
src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Feb 03 13:35:50 2014 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Feb 03 13:45:54 2014 +0100
@@ -458,8 +458,8 @@
   let
     val context = Context.Proof (Proof_Context.init_global thy);
     val marked = Idents.get context;
-    val (marked', context') = activate_all name thy Element.init
-      (Morphism.transfer_morphism o Context.theory_of) (empty_idents, context)
+    val (marked', context') = (empty_idents, context)
+      |> activate_all name thy Element.init (Morphism.transfer_morphism o Context.theory_of);
   in
     context'
     |> Idents.put (merge_idents (marked, marked'))