Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/local_theory.ML
changeset 28406 daeb21fec18f
parent 28395 984fcc8feb24
child 28965 1de908189869 
--- 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')
isabelle