src/Pure/Isar/bundle.ML
changeset 47070 15cd66da537f
parent 47069 451fc10a81f3
child 47249 c0481c3c2a6c
equal deleted inserted replaced
47069:451fc10a81f3 47070:15cd66da537f
    94   in #2 (Proof_Context.note_thmss "" [note] ctxt) end;
    94   in #2 (Proof_Context.note_thmss "" [note] ctxt) end;
    95 
    95 
    96 fun gen_context prep args (Context.Theory thy) =
    96 fun gen_context prep args (Context.Theory thy) =
    97       Named_Target.theory_init thy
    97       Named_Target.theory_init thy
    98       |> Local_Theory.target (gen_includes prep args)
    98       |> Local_Theory.target (gen_includes prep args)
       
    99       |> Local_Theory.restore
    99   | gen_context prep args (Context.Proof lthy) =
   100   | gen_context prep args (Context.Proof lthy) =
   100       Named_Target.assert lthy
   101       Named_Target.assert lthy
   101       |> gen_includes prep args
   102       |> gen_includes prep args
   102       |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
   103       |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
   103 
   104