author | wenzelm |
Mon, 02 Apr 2012 23:27:24 +0200 | |
changeset 48165 | d6c76b1823fb |
parent 48164 | d2367cc84235 |
child 48166 | 57d486231c92 |
1.1 --- a/src/Pure/Isar/local_theory.ML Mon Apr 02 21:52:03 2012 +0200 1.2 +++ b/src/Pure/Isar/local_theory.ML Mon Apr 02 23:27:24 2012 +0200 1.3 @@ -128,7 +128,7 @@ 1.4 |> Data.map (cons (make_lthy (naming, operations, target))); 1.5 1.6 fun close_target lthy = 1.7 - assert_bottom false lthy |> Data.map tl; 1.8 + assert_bottom false lthy |> Data.map tl |> restore; 1.9 1.10 fun map_contexts f lthy = 1.11 let val n = level lthy in