target update: invisible context position avoids duplication of reports etc.;

--- 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')