Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/toplevel.ML
changeset 71023 35a8e15b7e03
parent 70398 725438ceae7c
child 72434 cc27cf7e51c6 
--- a/src/Pure/Isar/toplevel.ML	Mon Nov 04 16:56:16 2019 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Nov 04 20:10:23 2019 +0100
@@ -294,7 +294,9 @@
       let
         val State ((node', pr_ctxt), _) =
           node |> apply
-            (fn _ => node_presentation (Theory (Context.Theory (Theory.end_theory thy))))
+            (fn _ =>
+              node_presentation
+                (Theory (Context.Theory (tap Thm.expose_theory (Theory.end_theory thy)))))
             (K ());
       in State ((Toplevel, pr_ctxt), get_theory node') end
   | (Keep f, node) =>
isabelle