src/Pure/Isar/isar_syn.ML
changeset 7002 01a4e15ee253
parent 6972 3ae2eeabde80
child 7012 ae9dac5af9d1
--- a/src/Pure/Isar/isar_syn.ML	Wed Jul 14 12:28:12 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jul 14 13:05:28 1999 +0200
@@ -343,23 +343,24 @@
 
 val qedP =
   OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
-    (Scan.option (P.method -- P.interest) >> IsarThy.qed);
+    (Scan.option (P.method -- P.interest) -- P.marg_comment >> IsarThy.qed);
 
 val terminal_proofP =
   OuterSyntax.command "by" "terminal backward proof" K.qed
-    (P.method -- P.interest -- Scan.option (P.method -- P.interest) >> IsarThy.terminal_proof);
+    (P.method -- P.interest -- Scan.option (P.method -- P.interest)
+      -- P.marg_comment >> IsarThy.terminal_proof);
 
 val immediate_proofP =
   OuterSyntax.command "." "immediate proof" K.qed
-    (Scan.succeed IsarThy.immediate_proof);
+    (P.marg_comment >> IsarThy.immediate_proof);
 
 val default_proofP =
   OuterSyntax.command ".." "default proof" K.qed
-    (Scan.succeed IsarThy.default_proof);
+    (P.marg_comment >> IsarThy.default_proof);
 
 val skip_proofP =
   OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
-    (Scan.succeed IsarThy.skip_proof);
+    (P.marg_comment >> IsarThy.skip_proof);
 
 
 (* proof steps *)
@@ -374,7 +375,7 @@
 
 val proofP =
   OuterSyntax.command "proof" "backward proof" K.prf_block
-    (P.interest -- Scan.option (P.method -- P.interest)
+    (P.interest -- Scan.option (P.method -- P.interest) -- P.marg_comment
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));