put_thms: ContextPosition.set_visible false;
authorwenzelm
Mon Sep 29 21:45:44 2008 +0200 (2008-09-29 ago)
changeset 2841774e580c6f2b5
parent 28416 263599f1346a
child 28418 4ffb62675ade
put_thms: ContextPosition.set_visible false;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Sep 29 21:26:49 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Sep 29 21:45:44 2008 +0200
     1.3 @@ -986,8 +986,12 @@
     1.4  fun note_thmss k = gen_note_thmss get_fact k;
     1.5  fun note_thmss_i k = gen_note_thmss (K I) k;
     1.6  
     1.7 -fun put_thms do_props thms ctxt =
     1.8 -  ctxt |> map_naming (K local_naming) |> update_thms do_props thms |> restore_naming ctxt;
     1.9 +fun put_thms do_props thms ctxt = ctxt
    1.10 +  |> map_naming (K local_naming)
    1.11 +  |> ContextPosition.set_visible false
    1.12 +  |> update_thms do_props thms
    1.13 +  |> ContextPosition.restore_visible ctxt
    1.14 +  |> restore_naming ctxt;
    1.15  
    1.16  end;
    1.17