# HG changeset patch
# User wenzelm
# Date 1466586618 -7200
# Node ID c8366fb67538e43b127929ec3b745bcb957d5e8a
# Parent  70b2313f9c52c1e702536a2f981b5b58a3e51735
clarified PIDE markup;

diff -r 70b2313f9c52 -r c8366fb67538 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed Jun 22 10:42:53 2016 +0200
+++ b/src/Pure/Isar/generic_target.ML	Wed Jun 22 11:10:18 2016 +0200
@@ -242,7 +242,9 @@
 
     (*local definition*)
     val ([(lhs, (_, local_def))], lthy3) = lthy2
-      |> Local_Defs.define [((b, NoSyn), (Thm.empty_binding, lhs'))];
+      |> Context_Position.set_visible false
+      |> Local_Defs.define [((b, NoSyn), (Thm.empty_binding, lhs'))]
+      ||> Context_Position.restore_visible lthy2;
 
     (*result*)
     val def =
@@ -329,8 +331,8 @@
   in
     lthy
     |> target_abbrev prmode (b, mx') global_rhs (type_params, term_params)
+    |> Context_Position.set_visible false
     |> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd
-    |> Context_Position.set_visible false
     |> Local_Defs.fixed_abbrev ((b, NoSyn), rhs)
     ||> Context_Position.restore_visible lthy
   end;