src/Pure/Isar/generic_target.ML

     val ((lhs', global_def), lthy2) = lthy
       |> foundation (((b, U), mx'), (b_def, rhs')) (type_params, term_params);
 
     (*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 =
       Thm.transitive local_def global_def
       |> Local_Defs.contract lthy3 defs (Thm.cterm_of lthy3 (Logic.mk_equals (lhs, rhs)));

     val (global_rhs, (extra_tfrees, (type_params, term_params))) = export_abbrev lthy I rhs;
     val mx' = check_mixfix lthy (b, extra_tfrees) mx;
   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;