changeset 70320 | 59258a3192bf |
parent 69593 | 3dda49e08b9d |
child 70323 | 2943934a169d |
70319:34bc296374ee | 70320:59258a3192bf |
---|---|
126 in |
126 in |
127 map_interrupt' f l [] |
127 map_interrupt' f l [] |
128 end |
128 end |
129 |
129 |
130 fun conceal_naming_result f lthy = |
130 fun conceal_naming_result f lthy = |
131 let val old_lthy = lthy |
131 lthy |> Proof_Context.concealed |> f ||> Proof_Context.restore_naming lthy; |
132 in lthy |> Proof_Context.concealed |> f ||> Proof_Context.restore_naming old_lthy end; |
|
133 |
132 |
134 end |
133 end |