# HG changeset patch
# User haftmann
# Date 1534505191 0
# Node ID 23a5e7fba8377ecf440361a2f228d9c8ddaeab35
# Parent  7e1978b9a4d1bbe3b9aac01d2b54150082d4eb09
tuned

diff -r 7e1978b9a4d1 -r 23a5e7fba837 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Aug 19 10:32:22 2018 +0200
+++ b/src/Pure/Isar/toplevel.ML	Fri Aug 17 11:26:31 2018 +0000
@@ -213,7 +213,7 @@
             Theory (gthy, _) => gthy
           | Proof (_, (_, gthy)) => gthy
           | Skipped_Proof (_, (_, gthy)) => gthy);
-        val lthy = Context.cases (Named_Target.theory_init) I gthy;
+        val lthy = Context.cases Named_Target.theory_init I gthy;
       in Local_Theory.pretty lthy end);
 
 fun pretty_state state =