diff -r e5128a9c4311 -r 213b9811f59f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Feb 25 23:14:51 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Feb 26 10:40:13 2014 +0100
@@ -620,11 +620,11 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "qed"} "conclude proof"
-    (Scan.option Method.parse >> Isar_Cmd.qed);
+    (Scan.option Method.parse_report >> Isar_Cmd.qed);
 
 val _ =
   Outer_Syntax.command @{command_spec "by"} "terminal backward proof"
-    (Method.parse -- Scan.option Method.parse >> Isar_Cmd.terminal_proof);
+    (Method.parse_report -- Scan.option Method.parse_report >> Isar_Cmd.terminal_proof);
 
 val _ =
   Outer_Syntax.command @{command_spec ".."} "default proof"
@@ -659,15 +659,15 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
-    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_results)));
+    (Method.parse_report >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_results)));
 
 val _ =
   Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)"
-    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end_results)));
+    (Method.parse_report >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end_results)));
 
 val _ =
   Outer_Syntax.command @{command_spec "proof"} "backward proof step"
-    (Scan.option Method.parse >> (fn m => Toplevel.print o
+    (Scan.option Method.parse_report >> (fn m => Toplevel.print o
       Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
       Toplevel.skip_proof (fn i => i + 1)));