src/Pure/Isar/proof_context.ML
changeset 28417 74e580c6f2b5
parent 28411 93ec7fa3b3a0
child 28792 1d80cee865de
     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