# HG changeset patch
# User wenzelm
# Date 1512741834 -3600
# Node ID 0050cd50936db315012de5f13a2f04e818f6451c
# Parent  b762ed417ed90cbb51c8706c92e97bce556db8bb
uniform use of original theory;

diff -r b762ed417ed9 -r 0050cd50936d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Dec 08 14:39:52 2017 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Dec 08 15:03:54 2017 +0100
@@ -187,7 +187,7 @@
           (case node of
             Theory (gthy, _) => gthy
           | Proof (_, (_, gthy)) => gthy
-          | Skipped_Proof (_, (gthy, _)) => gthy);
+          | Skipped_Proof (_, (_, gthy)) => gthy);
         val lthy = Context.cases (Named_Target.theory_init) I gthy;
       in Local_Theory.pretty lthy end);