changeset 47281 | d6c76b1823fb |
parent 47273 | ea089b484157 |
child 49042 | 01041f7bf9b4 |
--- a/src/Pure/Isar/local_theory.ML Mon Apr 02 21:52:03 2012 +0200 +++ b/src/Pure/Isar/local_theory.ML Mon Apr 02 23:27:24 2012 +0200 @@ -128,7 +128,7 @@ |> Data.map (cons (make_lthy (naming, operations, target))); fun close_target lthy = - assert_bottom false lthy |> Data.map tl; + assert_bottom false lthy |> Data.map tl |> restore; fun map_contexts f lthy = let val n = level lthy in