From 22bc319440ee852246a5ff67fbc684e0be9d80ac Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 7 Feb 2012 17:19:05 +0000
Subject: Load pg_tactics, fix proof-undo-n-times-cmd again.

---
 hol-light/hol-light.el | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el
index 9c9dbc5c..d7ab7385 100644
--- a/hol-light/hol-light.el
+++ b/hol-light/hol-light.el
@@ -41,14 +41,17 @@ You need to restart Emacs if you change this setting."
   :type 'boolean
   :group 'hol-light)
 
-
 (defconst hol-light-pre-sync-cmd
   (format "#use \"%s/hol-light/pg_prompt.ml\";; " proof-home-directory)
   "Command used to configure prompt annotations for Proof General.")
 
 (defcustom hol-light-init-cmd 
-  (list (format "#cd \"%s\"" hol-light-home)
-	"#use \"hol.ml\"")
+  (append
+   (list (format "#cd \"%s\"" hol-light-home)
+	 "#use \"hol.ml\"")
+   (if hol-light-use-custom-toplevel
+       (list (format "#use \"%shol-light/pg_tactics.ml\""
+		     proof-home-directory))))
   "*Commands used to start up a running HOL Light session."
   :type '(list string)
   :group 'hol-light)
@@ -158,7 +161,7 @@ You need to restart Emacs if you change this setting."
  proof-save-command            	"val %s = top_thm();;"
  proof-kill-goal-command       	"current_goalstack:=[];;" ; for cleanliness
  proof-showproof-command       	"p()"
- proof-undo-n-times-cmd        	"(funpow %s b; p());;"
+ proof-undo-n-times-cmd        	"(funpow %s (fun ()->let _ = b() in ()); p());;"
  proof-auto-multiple-files     	t
  proof-shell-cd-cmd            	"#cd \"%s\";;"
  proof-shell-filename-escapes  	'(("\\\\" . "\\\\") ("\""   . "\\\""))
-- 
cgit v1.2.3