# HG changeset patch
# User wenzelm
# Date 979846738 -3600
# Node ID 6ef388cedd584125e3ce21ae6fab5b59976f522f
# Parent  0b3997a180dd9466cb1b2334d12a1c419794bf6b
show/thus: Toplevel.proof';

diff -r 0b3997a180dd -r 6ef388cedd58 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Jan 18 20:38:32 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jan 18 20:38:58 2001 +0100
@@ -295,7 +295,7 @@
 
 val showP =
   OuterSyntax.command "show" "state local goal, solving current obligation" K.prf_goal
-    (statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof f));
+    (statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof' f));
 
 val haveP =
   OuterSyntax.command "have" "state local goal" K.prf_goal
@@ -303,7 +303,7 @@
 
 val thusP =
   OuterSyntax.command "thus" "abbreviates \"then show\"" K.prf_goal
-    (statement IsarThy.thus >> (fn f => Toplevel.print o Toplevel.proof f));
+    (statement IsarThy.thus >> (fn f => Toplevel.print o Toplevel.proof' f));
 
 val henceP =
   OuterSyntax.command "hence" "abbreviates \"then have\"" K.prf_goal