put_thms: ContextPosition.set_visible false;
authorwenzelm
Mon, 29 Sep 2008 21:45:44 +0200
changeset 28417 74e580c6f2b5
parent 28416 263599f1346a
child 28418 4ffb62675ade
put_thms: ContextPosition.set_visible false;
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;