src/Pure/Isar/bundle.ML
changeset 66336 13e7dc5f7c3d
parent 66335 a849ce33923d
child 66337 5caea089dd17
--- a/src/Pure/Isar/bundle.ML	Fri Aug 04 08:12:54 2017 +0200
+++ b/src/Pure/Isar/bundle.ML	Fri Aug 04 08:12:57 2017 +0200
@@ -217,8 +217,8 @@
       |> prep_decl ([], []) I raw_elems;
   in
     lthy' |> Local_Theory.init_target
-      {background_naming = Local_Theory.background_naming_of lthy, after_close = after_close,
-       exit = Local_Theory.exit_of lthy} (Local_Theory.operations_of lthy)
+      {background_naming = Local_Theory.background_naming_of lthy, after_close = after_close}
+      (Local_Theory.operations_of lthy)
   end;
 
 in