# HG changeset patch
# User wenzelm
# Date 1222692084 -7200
# Node ID daeb21fec18fb519ee62e9b98763ccc53070b87d
# Parent  000dee6d5d80af1c0cc35b8039396975b2a0e974
target update: invisible context position avoids duplication of reports etc.;

diff -r 000dee6d5d80 -r daeb21fec18f src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Mon Sep 29 14:41:23 2008 +0200
+++ b/src/Pure/Isar/local_theory.ML	Mon Sep 29 14:41:24 2008 +0200
@@ -154,7 +154,10 @@
 
 fun target_result f lthy =
   let
-    val (res, ctxt') = f (target_of lthy);
+    val (res, ctxt') = target_of lthy
+      |> ContextPosition.set_visible false
+      |> f
+      ||> ContextPosition.restore_visible lthy;
     val thy' = ProofContext.theory_of ctxt';
     val lthy' = lthy
       |> map_target (K ctxt')