--- a/src/Pure/Isar/toplevel.ML Thu Dec 07 15:48:50 2017 +0100
+++ b/src/Pure/Isar/toplevel.ML Thu Dec 07 19:36:48 2017 +0100
@@ -455,7 +455,8 @@
(fn Theory (gthy, _) =>
let
val (finish, prf) = init int gthy;
- val skip = Goal.skip_proofs_enabled ();
+ 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;
val _ =
if skip andalso schematic_goal = SOME true then