Fix compile errors

4 files changed, 37 insertions, 26 deletions

diff --git a/isar/Example.thy b/isar/Example.thy
index 720e5480..b0640146 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -9,10 +9,10 @@ theory Example imports Main begin
 
 text {* Proper proof text -- \textit{naive version}. *}
 
-theorem and_comms: "A & B --> B & A"
+theorem and_comms: "A \<and> B \<longrightarrow> B \<and> A"
 proof
-  assume "A & B"
-  then show "B & A"
+  assume "A \<and> B"
+  then show "B \<and> A"
   proof
     assume B and A
     then show ?thesis ..
@@ -22,6 +22,9 @@ qed
 text {* Unstructured proof script. *}
 
 theorem  "A & B --> B & A"
+by and_comms
+
+
   apply (rule impI)
   apply (erule conjE)
   apply (rule conjI)
diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el
index cc5d51d7..4ea027be 100644
--- a/isar/isar-autotest.el
+++ b/isar/isar-autotest.el
@@ -6,6 +6,9 @@
 ;;
 
 (eval-when-compile
+  (require 'cl))
+
+(eval-when (compile)
   (require 'proof-utils)
   (proof-ready-for-assistant 'isar))
 
diff --git a/isar/isar-find-theorems.el b/isar/isar-find-theorems.el
index 0d40f392..15da9f67 100644
--- a/isar/isar-find-theorems.el
+++ b/isar/isar-find-theorems.el
@@ -10,6 +10,23 @@
 ;; $Id$
 ;;
 
+(require 'pg-vars)
+(declare-function proof-find-theorems "pg-user")
+
+
+;; search form field values
+
+(defvar isar-find-theorems-data (list
+  ""      ;; num
+  ""      ;; pattern
+  "none"  ;; intro
+  "none"  ;; elim
+  "none"  ;; dest
+  ""      ;; name
+  ""      ;; simp
+  )
+  "Values of the Find Theorems search form's fields.")
+
 ;; make the original (minibuffer based) "Find theorems" command (from
 ;; ../generic/pg-user.el) available as isar-find-theorems-minibuffer;
 ;; return '(nil) so that isar-find-theorems-minibuffer works as a
@@ -35,7 +52,7 @@
   (apply 'isar-find-theorems-create-searchform isar-find-theorems-data)
   '(nil))
 
-;; update the universal key bindings (see ../generic/proof-config.el)
+;; update the universal key bindings (see ../generic/pg-vars.el)
 ;;
 ;; C-c C-a C-m is bound to isar-find-theorems-minibuffer
 ;; C-c C-a C-f is bound to isar-find-theorems-form
@@ -69,19 +86,6 @@
 ;; matching the current goal as introduction rule and not having "HOL."
 ;; in their name (i.e. not being defined in theory HOL).
 
-;; search form field values
-
-(defvar isar-find-theorems-data (list
-  ""      ;; num
-  ""      ;; pattern
-  "none"  ;; intro
-  "none"  ;; elim
-  "none"  ;; dest
-  ""      ;; name
-  ""      ;; simp
-  )
-  "Values of the Find Theorems search form's fields.")
-
 ;; search form widgets (set in isar-find-theorems-create-searchform
 ;; and accessed in the "Find" handler)
 
diff --git a/isar/isar.el b/isar/isar.el
index 0455ec6d..719d7ce7 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -593,15 +593,16 @@ This slows down interactive processing slightly."
 (defun isar-preprocessing ()
   "Insert sync markers and other hacks.
 Uses variables `string' and `scriptspan' passed by dynamic scoping."
-  (if (proof-string-match isabelle-verbatim-regexp string)
-      (setq string (match-string 1 string))
-    (unless (string-match ";[ \t]*\\'" string)
-      (setq string (concat string ";")))
-    (setq string (concat
-		  "\\<^sync>; "
-		  (isar-shell-adjust-line-width)
-		  string
-		  " \\<^sync>;"))))
+  (with-no-warnings  ; dynamic scoping of string, scriptspan
+    (if (proof-string-match isabelle-verbatim-regexp string)
+	(setq string (match-string 1 string))
+      (unless (string-match ";[ \t]*\\'" string)
+	(setq string (concat string ";")))
+      (setq string (concat
+		    "\\<^sync>; "
+		    (isar-shell-adjust-line-width)
+		    string
+		    " \\<^sync>;")))))
 
 ;;
 ;;   Configuring proof output buffer