src/Pure/Isar/isar_syn.ML

     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
 
 val endP =
   OuterSyntax.command "}" "end explicit proof block"
     (K.tag_proof K.prf_close)
-    (Scan.succeed (Toplevel.print o Toplevel.proofs Proof.end_block));
+    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
 
 val nextP =
   OuterSyntax.command "next" "enter next proof block"
     (K.tag_proof K.prf_block)
     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));