merged

--- a/src/Pure/Thy/thy_output.ML	Tue May 15 21:19:22 2018 +0200
+++ b/src/Pure/Thy/thy_output.ML	Wed May 16 15:52:15 2018 +0200
@@ -117,13 +117,14 @@
       |> maps output_symbols_antiq
   | (SOME comment, _) => output_comment ctxt (comment, syms));
 
-in
-
 fun output_body ctxt antiq bg en syms =
   Comment.read_body syms
   |> maps (output_comment_symbols ctxt {antiq = antiq})
-  |> Latex.enclose_body bg en
-and output_token ctxt tok =
+  |> Latex.enclose_body bg en;
+
+in
+
+fun output_token ctxt tok =
   let
     fun output antiq bg en =
       output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok));

--- a/src/Pure/context.ML	Tue May 15 21:19:22 2018 +0200
+++ b/src/Pure/context.ML	Wed May 16 15:52:15 2018 +0200
@@ -177,7 +177,7 @@
 fun display_names thy =
   let
     val name = display_name (theory_id thy);
-    val ancestor_names = map theory_name (ancestors_of thy);
+    val ancestor_names = map theory_long_name (ancestors_of thy);
   in rev (name :: ancestor_names) end;
 
 val pretty_thy = Pretty.str_list "{" "}" o display_names;
@@ -359,7 +359,7 @@
 
 val update_thy = change_thy false;
 val extend_thy = update_thy I;
-val finish_thy = change_thy true I;
+val finish_thy = change_thy true I #> tap extend_thy;
 
 end;
 
@@ -399,7 +399,7 @@
 
       val history = make_history name 0;
       val ancestry = make_ancestry parents ancestors;
-    in create_thy ids history ancestry (data_of thy0) end;
+    in create_thy ids history ancestry (data_of thy0) |> tap finish_thy end;
 
 end;