# HG changeset patch
# User wenzelm
# Date 1222717544 -7200
# Node ID 74e580c6f2b5facfae244ebb42977a11998346b8
# Parent  263599f1346ac80c72ab2f451546f62403fc5cc3
put_thms: ContextPosition.set_visible false;

diff -r 263599f1346a -r 74e580c6f2b5 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Sep 29 21:26:49 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Sep 29 21:45:44 2008 +0200
@@ -986,8 +986,12 @@
 fun note_thmss k = gen_note_thmss get_fact k;
 fun note_thmss_i k = gen_note_thmss (K I) k;
 
-fun put_thms do_props thms ctxt =
-  ctxt |> map_naming (K local_naming) |> update_thms do_props thms |> restore_naming ctxt;
+fun put_thms do_props thms ctxt = ctxt
+  |> map_naming (K local_naming)
+  |> ContextPosition.set_visible false
+  |> update_thms do_props thms
+  |> ContextPosition.restore_visible ctxt
+  |> restore_naming ctxt;
 
 end;