# HG changeset patch
# User haftmann
# Date 1602355390 0
# Node ID 166fc8b9b4cd587164b0f6caefa62327e1ab9986
# Parent  cc27cf7e51c62e6460ce8577e0b91ede55b1b392
tuned

diff -r cc27cf7e51c6 -r 166fc8b9b4cd src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Sat Oct 10 18:43:09 2020 +0000
+++ b/src/Pure/Isar/bundle.ML	Sat Oct 10 18:43:10 2020 +0000
@@ -208,14 +208,18 @@
 
 fun gen_context get prep_decl raw_incls raw_elems gthy =
   let
-    val (after_close, lthy) =
-      gthy |> Context.cases (pair Local_Theory.exit o Named_Target.theory_init)
-        (pair I o Local_Theory.assert);
-    val ((_, _, _, lthy'), _) = lthy
-      |> gen_includes get raw_incls
-      |> prep_decl ([], []) I raw_elems;
+    val init = Context.cases
+      (pair Local_Theory.exit o Named_Target.theory_init)
+      (pair I o Local_Theory.assert);
+    val import =
+      gen_includes get raw_incls
+      #> prep_decl ([], []) I raw_elems
+      #> (#4 o fst);
   in
-    lthy' |> Local_Theory.begin_target after_close
+    gthy
+    |> init
+    ||> import
+    |-> (fn after_close => Local_Theory.begin_target after_close)
   end;
 
 in