src/Pure/Isar/toplevel.ML
changeset 67157 d0657c8b7616
parent 66169 8cfa8c7ee1f6
child 67162 0050cd50936d
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Jun 22 21:44:15 2017 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Dec 07 19:36:48 2017 +0100
     1.3 @@ -455,7 +455,8 @@
     1.4    (fn Theory (gthy, _) =>
     1.5      let
     1.6        val (finish, prf) = init int gthy;
     1.7 -      val skip = Goal.skip_proofs_enabled ();
     1.8 +      val document = Options.default_string "document";
     1.9 +      val skip = (document = "" orelse document = "false") andalso Goal.skip_proofs_enabled ();
    1.10        val schematic_goal = try Proof.schematic_goal prf;
    1.11        val _ =
    1.12          if skip andalso schematic_goal = SOME true then