author | wenzelm |
Mon, 02 Apr 2012 23:27:24 +0200 | |
changeset 47281 | d6c76b1823fb |
parent 47280 | d2367cc84235 |
child 47282 | 57d486231c92 |
--- 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