# HG changeset patch
# User wenzelm
# Date 1552123880 -3600
# Node ID a9e574e2cba52d41dfdc45256a3c929f401dcd9d
# Parent  2731278dfff973269f71c6f52f4489b033c55e75
tuned;

diff -r 2731278dfff9 -r a9e574e2cba5 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Mar 08 18:56:48 2019 +0000
+++ b/src/Pure/Isar/toplevel.ML	Sat Mar 09 10:31:20 2019 +0100
@@ -480,10 +480,10 @@
 
 local
 
-fun begin_proof init = transaction0 (fn int =>
+fun begin_proof init_proof = transaction0 (fn int =>
   (fn Theory gthy =>
     let
-      val (finish, prf) = init int gthy;
+      val (finish, prf) = init_proof int gthy;
       val document = Options.default_string "document";
       val skip = (document = "" orelse document = "false") andalso Goal.skip_proofs_enabled ();
       val schematic_goal = try Proof.schematic_goal prf;