src/Pure/Isar/toplevel.ML
changeset 70063 a9e574e2cba5
parent 70059 ccc8e4c99520
child 70064 f8293bf510a0
     1.1 --- a/src/Pure/Isar/toplevel.ML	Fri Mar 08 18:56:48 2019 +0000
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Mar 09 10:31:20 2019 +0100
     1.3 @@ -480,10 +480,10 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun begin_proof init = transaction0 (fn int =>
     1.8 +fun begin_proof init_proof = transaction0 (fn int =>
     1.9    (fn Theory gthy =>
    1.10      let
    1.11 -      val (finish, prf) = init int gthy;
    1.12 +      val (finish, prf) = init_proof int gthy;
    1.13        val document = Options.default_string "document";
    1.14        val skip = (document = "" orelse document = "false") andalso Goal.skip_proofs_enabled ();
    1.15        val schematic_goal = try Proof.schematic_goal prf;