Fix for splash hack for theory files when proo-splash-inhibit=t.

2 files changed, 2 insertions, 2 deletions

diff --git a/isa/example.ML b/isa/example.ML
index 11b807f4..a8922e87 100644
--- a/isa/example.ML
+++ b/isa/example.ML
@@ -14,7 +14,6 @@ br conjI 1;
 be conjE 1;
 ba 1;
 be conjE 1;
-ba 45;
 ba 1;
 qed "and_comms";
 
diff --git a/isa/isa.el b/isa/isa.el
index f5d6158f..960d2730 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -343,7 +343,8 @@ isa-proofscript-mode."
 	 (string-match ".thy" (buffer-file-name)))
     (thy-mode)
     ;; Hack for splash screen
-    (if (memq 'proof-splash-timeout-waiter proof-mode-hook)
+    (if (and proof-mode-hook
+	     (memq 'proof-splash-timeout-waiter proof-mode-hook))
 	(proof-splash-timeout-waiter))
     ;; Has this theory file already been loaded by Isabelle?
     ;; Colour it blue if so.