Clean whitespace

7 files changed, 117 insertions, 117 deletions

diff --git a/isar/Example.thy b/isar/Example.thy
index 34c840fe..720e5480 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -4,6 +4,7 @@
       $Id$
 *)
 
+
 theory Example imports Main begin
 
 text {* Proper proof text -- \textit{naive version}. *}
@@ -28,4 +29,5 @@ theorem  "A & B --> B & A"
   apply assumption
 done
 
+
 end
diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el
index e206822a..a370654e 100644
--- a/isar/isabelle-system.el
+++ b/isar/isabelle-system.el
@@ -43,7 +43,7 @@
       (getenv "ISABELLE_TOOL")
       (proof-locate-executable "isabelle" nil
 			       (list
-				;; support default unpack in home dir situation 
+				;; support default unpack in home dir situation
 				(concat (getenv "HOME") "/Isabelle/bin/")))
       "path_to_isabelle_is_unknown")
   "Command to invoke the main Isabelle wrapper 'isabelle'.
@@ -61,12 +61,12 @@ working."
   "Make sure `isa-isabelle-command' points to a valid executable.
 If it does not, or if prefix arg supplied, prompt the user for
 the proper setting.  If `proof-rsh-command' is set, leave this
-unverified.  Otherwise, returns non-nil if isa-isabelle-command 
+unverified.  Otherwise, returns non-nil if isa-isabelle-command
 is surely an executable with full path."
   (interactive "p")
   (when (and (not noninteractive)
 	     (not proof-rsh-command)
-	     (or force 
+	     (or force
 		 isabelle-not-found
 		 (not (file-executable-p isa-isabelle-command))))
     (setq isa-isabelle-command
@@ -155,17 +155,17 @@ at the top of your theory file, like this:
 
 (defvar isabelle-chosen-logic-prev nil
   "Value of `isabelle-chosen-logic' on last call of `isabelle-set-prog-name'.")
-  
+
 (defun isabelle-hack-local-variables-function ()
   "Hook function for `hack-local-variables-hook'."
   (if (and isabelle-chosen-logic
-	   (not (equal isabelle-chosen-logic 
+	   (not (equal isabelle-chosen-logic
 		       isabelle-chosen-logic-prev))
 	   (proof-shell-live-buffer))
       (message "Warning: chosen logic %s does not match running Isabelle instance"
 	       isabelle-chosen-logic)))
 
-(add-hook 'hack-local-variables-hook 
+(add-hook 'hack-local-variables-hook
 	  'isabelle-hack-local-variables-function)
 
 (defun isabelle-set-prog-name (&optional filename)
@@ -177,9 +177,9 @@ This function sets `isabelle-prog-name' and `proof-prog-name'."
       ;; is set in current Isabelle settings environment.
       ((isabelle (or
 		  isabelle-program-name-override  ; override in Emacs
-		  (getenv "ISABELLE_PROCESS")	  ; command line override 
+		  (getenv "ISABELLE_PROCESS")	  ; command line override
 		  (isa-getenv "ISABELLE_PROCESS") ; choose to match isabelle
-		  "isabelle-process"))		  ; to 
+		  "isabelle-process"))		  ; to
        (isabelle-opts (getenv "ISABELLE_OPTIONS"))
        (opts (concat " -PI"  ;; Proof General + Isar
 	      (if proof-shell-unicode " -m PGASCII" "")
@@ -218,7 +218,7 @@ This function sets `isabelle-prog-name' and `proof-prog-name'."
       (apply 'start-process
 	     "isa-view-doc" nil
 	     (append (split-string
-		      isa-isabelle-command) 
+		      isa-isabelle-command)
 		     (list "doc" docname)))))
 
 (defun isa-tool-list-docs ()
@@ -257,7 +257,7 @@ for you, you should disable this behaviour."
   :type 'boolean
   :group 'isabelle)
 
-(defvar isabelle-docs-menu 
+(defvar isabelle-docs-menu
   (let ((vc '(lambda (docdes)
 	       (vector (car (cdr docdes))
 		       (list 'isa-view-doc (car docdes)) t))))
@@ -311,7 +311,7 @@ for you, you should disable this behaviour."
   "Update logics menu."
   (and (current-local-map)
        (keymapp (lookup-key (current-local-map)
- 			    (vector 'menu-bar (intern proof-assistant))))
+			    (vector 'menu-bar (intern proof-assistant))))
        (isabelle-logics-menu-refresh)))
 
 (add-hook 'menu-bar-update-hook 'isabelle-menu-bar-update-logics)
diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el
index 8d6aae95..da83aabb 100644
--- a/isar/isar-autotest.el
+++ b/isar/isar-autotest.el
@@ -30,8 +30,6 @@
   (pg-autotest assert-unprocessed "etc/isar/multiple/C.thy")
   (pg-autotest assert-processed   "etc/isar/multiple/A.thy")
 
-  
+
   (pg-autotest-quit-prover)
   (pg-autotest-finished))
-
-
diff --git a/isar/isar-find-theorems.el b/isar/isar-find-theorems.el
index 2e007e78..0d40f392 100644
--- a/isar/isar-find-theorems.el
+++ b/isar/isar-find-theorems.el
@@ -122,7 +122,7 @@
   (widget-insert
     (concat "\n  "
       (if (fboundp 'propertize)
-        (propertize "Find Theorems" 'face 'bold)
+	(propertize "Find Theorems" 'face 'bold)
       "Find Theorems")
       "\n\n"))
 
@@ -190,7 +190,7 @@
   (widget-create 'push-button
     :help-echo "Click <mouse-2> for help."
     :notify (lambda (&rest ignore) (isar-find-theorems-create-help))
-    "?")  
+    "?")
 
   ;; num
   (widget-insert "\n\n  Number of results:      ")
@@ -210,15 +210,15 @@
     :help-echo "Click <mouse-2> to submit this form."
     :notify (lambda (&rest ignore)
       (let ((num     (widget-value isar-find-theorems-widget-number))
-            (pattern (widget-value isar-find-theorems-widget-pattern))
-            (intro   (widget-value isar-find-theorems-widget-intro))
-            (elim    (widget-value isar-find-theorems-widget-elim))
-            (dest    (widget-value isar-find-theorems-widget-dest))
-            (name    (widget-value isar-find-theorems-widget-name))
-            (simp    (widget-value isar-find-theorems-widget-simp)))
+	    (pattern (widget-value isar-find-theorems-widget-pattern))
+	    (intro   (widget-value isar-find-theorems-widget-intro))
+	    (elim    (widget-value isar-find-theorems-widget-elim))
+	    (dest    (widget-value isar-find-theorems-widget-dest))
+	    (name    (widget-value isar-find-theorems-widget-name))
+	    (simp    (widget-value isar-find-theorems-widget-simp)))
       (kill-buffer "*Find Theorems*")
       (isar-find-theorems-submit-searchform
-        num pattern intro elim dest name simp)))
+	num pattern intro elim dest name simp)))
     "Find")
 
   ;; Reset form
@@ -228,7 +228,7 @@
     :notify (lambda (&rest ignore)
       (kill-buffer "*Find Theorems*")
       (isar-find-theorems-create-searchform
-        "" "" "none" "none" "none" "" ""))
+	"" "" "none" "none" "none" "" ""))
     "Reset Form")
     (widget-insert "\n")
 
@@ -236,7 +236,7 @@
   (if errmsg
     (widget-insert (concat "\n    "
       (if (fboundp 'propertize)
-        (propertize (concat errmsg "\n    See help for details.") 'face 'bold)
+	(propertize (concat errmsg "\n    See help for details.") 'face 'bold)
       (concat errmsg "\n    See help for details."))
       "\n")))
 
@@ -351,7 +351,7 @@
   (setq searchstring (format "find_theorems %s"
     (mapconcat 'identity
       (isar-find-theorems-filter-empty
-        (list num_ pattern_ intro_ elim_ dest_ name_ simp_))
+	(list num_ pattern_ intro_ elim_ dest_ name_ simp_))
       " ")))
 
   ;; note that proof-find-theorems with an argument provided
@@ -391,30 +391,30 @@ escaped by double-quotes."
     ;;       well.
     (if (equal (elt criteria-string 0) ?-)
       (progn
-        (setq tokens (cons "-" tokens))
-        (setq criteria-string (substring criteria-string 1)))
+	(setq tokens (cons "-" tokens))
+	(setq criteria-string (substring criteria-string 1)))
 
     ;; " starts a token: search for the next ", regard as one token
     ;; Note: This is still a bit weird, as it does not require the
     ;;       closing double-quotes to be followed by a space. Oh well.
     (if (equal (elt criteria-string 0) ?\")
       (let ((i 1))
-        (while (and (< i (length criteria-string))
-                    (not (equal (elt criteria-string i) ?\")))
-          (setq i (1+ i)))
-        (if (equal i (length criteria-string))
-          (setq errmsg "missing closing double-quotes.")
-        (setq i (1+ i))
-        (setq tokens (cons (substring criteria-string 0 i) tokens))
-        (setq criteria-string (substring criteria-string i))))
+	(while (and (< i (length criteria-string))
+		    (not (equal (elt criteria-string i) ?\")))
+	  (setq i (1+ i)))
+	(if (equal i (length criteria-string))
+	  (setq errmsg "missing closing double-quotes.")
+	(setq i (1+ i))
+	(setq tokens (cons (substring criteria-string 0 i) tokens))
+	(setq criteria-string (substring criteria-string i))))
 
     ;; everything else: search for the next space, regard as one token
     ;; Note: This is still a bit weird, as it scans over double-quotes.
     ;;       Oh well.
     (let ((i 1))
       (while (and (< i (length criteria-string))
-                  (not (equal (elt criteria-string i) ?\ )))
-        (setq i (1+ i)))
+		  (not (equal (elt criteria-string i) ?\ )))
+	(setq i (1+ i)))
       (setq tokens (cons (substring criteria-string 0 i) tokens))
       (setq criteria-string (substring criteria-string i)))
     )))
@@ -433,13 +433,13 @@ escaped by double-quotes."
     (let ((token (car tokens)))
     (if (equal token "-")
       (if negated
-        (setq errmsg "- may not be followed by another -.")
+	(setq errmsg "- may not be followed by another -.")
       (setq negated t)
       (setq tokens (cdr tokens)))
     (setq strings (cons
       (concat (if negated "-" "") option-string
-        ;; wrap token in double-quotes if necessary
-        (if (equal (elt token 0) ?\") token (concat "\"" token "\"")))
+	;; wrap token in double-quotes if necessary
+	(if (equal (elt token 0) ?\") token (concat "\"" token "\"")))
       strings))
     (setq negated nil)
     (setq tokens (cdr tokens))))
diff --git a/isar/isar-keywords.el b/isar/isar-keywords.el
index d42c682e..c7e0c7c2 100644
--- a/isar/isar-keywords.el
+++ b/isar/isar-keywords.el
@@ -1,5 +1,5 @@
 ;; NB: this copy of isar-keywords is NOT usually the one that is loaded.
-;; It will only be used if Isabelle is not properly installed and the 
+;; It will only be used if Isabelle is not properly installed and the
 ;; isatool command cannot be found.  It is needed as a fallback in this case.
 ;;
 ;; =================================================================
diff --git a/isar/isar-mmm.el b/isar/isar-mmm.el
index a36b484e..3ecc9f7b 100644
--- a/isar/isar-mmm.el
+++ b/isar/isar-mmm.el
@@ -5,11 +5,11 @@
 ;; Licence:	 GPL
 ;;
 ;; $Id$
-;; 
+;;
 ;; Presently, we deal with several cases of {* text *}.
 ;; It's not a good idea to do too much, since searching for the
 ;; regions and fontifying them is slow.
-;; 
+;;
 ;; TODO:
 ;;  --- fontification for antiquotations has been lost, could
 ;;      add that into LaTeX mode somehow.
@@ -21,22 +21,22 @@
 (require 'mmm-auto)
 (require 'proof-syntax)			; proof-ids-to-regexp
 
-(defconst isar-start-latex-regexp 
+(defconst isar-start-latex-regexp
   (concat
-   "\\(" 
-   (proof-ids-to-regexp 
+   "\\("
+   (proof-ids-to-regexp
     ;; Perhaps section is too much?  The fontification is nice but
     ;; section headers are a bit short to use LaTeX mode in.
-    (list "text" "header" ".*section"))  
+    (list "text" "header" ".*section"))
    ;; Next one is nice but hammers font lock a bit too much
    ;; if there are lots of -- {* short comments *}
    ;; "\\|\-\-" ;; NB: doesn't work with \\<--\\>
    "\\)[ \t]+{\\*"))
 
-(defconst isar-start-sml-regexp 
+(defconst isar-start-sml-regexp
   (concat
-   "\\(" 
-   (proof-ids-to-regexp 
+   "\\("
+   (proof-ids-to-regexp
     (list "ML" "ML_command" "ML_setup" "typed_print_translation"))
    "\\)[ \t]+{\\*"))
 
@@ -46,7 +46,7 @@
  `((isar-latex
    :submode LaTeX-mode
    :face mmm-comment-submode-face
-   :front ,isar-start-latex-regexp 
+   :front ,isar-start-latex-regexp
    :back  "\\*}"
    :insert ((?t isar-text nil @ "text {*" @ " " _ " " @ "*}" @)
 	    (?t isar-text_raw nil @ "text_raw {*" @ " " _ " " @ "*}" @)
@@ -62,7 +62,7 @@
 	    (?c isar-ML-command nil @ "ML_command {*" @ " " _ " " @ "*}" @)
 	    (?m isar-ML nil @ "ML {*" @ " " _ " " @ "*}" @)
 	    (?p isar-print-trans nil @ "typed_print_translation {*" @ " " _ " " @ "*}" @)))))
-	    
+
 
 (provide 'isar-mmm)
 
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 1af9e545..2e024eac 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -42,7 +42,7 @@ This list is in the right format for proof-easy-config.")
 (defconst isar-script-syntax-table-alist
   ;; NB: this is used for imenu.  Probably only need word syntax
   (let ((syn isar-script-syntax-table-entries)
-        al)
+	al)
     (while syn
       (setq al (cons (cons (char-to-string (car syn)) (cadr syn)) al))
       (setq syn (cddr syn)))
@@ -78,74 +78,74 @@ This list is in the right format for proof-easy-config.")
 (defconst isar-keywords-theory-enclose
   (append isar-keywords-theory-begin
 	  isar-keywords-theory-switch
-          isar-keywords-theory-end))
+	  isar-keywords-theory-end))
 
 (defconst isar-keywords-theory
   (append isar-keywords-theory-heading
-          isar-keywords-theory-decl
-          isar-keywords-theory-goal))
+	  isar-keywords-theory-decl
+	  isar-keywords-theory-goal))
 
 (defconst isar-keywords-save
   (append isar-keywords-qed
-          isar-keywords-qed-block
-          isar-keywords-qed-global))
+	  isar-keywords-qed-block
+	  isar-keywords-qed-global))
 
 (defconst isar-keywords-proof-enclose
   (append isar-keywords-proof-block
-          isar-keywords-proof-open
-          isar-keywords-proof-close
-          isar-keywords-qed-block))
+	  isar-keywords-proof-open
+	  isar-keywords-proof-close
+	  isar-keywords-qed-block))
 
 (defconst isar-keywords-proof
   (append isar-keywords-proof-heading
-          isar-keywords-proof-goal
-          isar-keywords-proof-chain
-          isar-keywords-proof-decl
-          isar-keywords-qed))
+	  isar-keywords-proof-goal
+	  isar-keywords-proof-chain
+	  isar-keywords-proof-decl
+	  isar-keywords-qed))
 
 (defconst isar-keywords-proof-context
   (append isar-keywords-proof-asm
-          isar-keywords-proof-asm-goal))
+	  isar-keywords-proof-asm-goal))
 
 (defconst isar-keywords-local-goal
   (append isar-keywords-proof-goal
-          isar-keywords-proof-asm-goal))
+	  isar-keywords-proof-asm-goal))
 
 (defconst isar-keywords-proper
   (append isar-keywords-theory
-          isar-keywords-proof-enclose
-          isar-keywords-proof))
+	  isar-keywords-proof-enclose
+	  isar-keywords-proof))
 
 (defconst isar-keywords-improper
   (append isar-keywords-theory-script
-          isar-keywords-proof-script
-          isar-keywords-qed-global))
+	  isar-keywords-proof-script
+	  isar-keywords-qed-global))
 
 (defconst isar-keywords-outline
   isar-keywords-theory-heading)
 
 (defconst isar-keywords-fume
   (append isar-keywords-theory-begin
-          isar-keywords-theory-heading
-          isar-keywords-theory-decl
-          isar-keywords-theory-script
-          isar-keywords-theory-goal))
+	  isar-keywords-theory-heading
+	  isar-keywords-theory-decl
+	  isar-keywords-theory-script
+	  isar-keywords-theory-goal))
 
 (defconst isar-keywords-indent-open
   (append isar-keywords-theory-goal
-          isar-keywords-proof-goal
-          isar-keywords-proof-asm-goal
-          isar-keywords-proof-open))
+	  isar-keywords-proof-goal
+	  isar-keywords-proof-asm-goal
+	  isar-keywords-proof-open))
 
 (defconst isar-keywords-indent-close
   (append isar-keywords-save
-          isar-keywords-proof-close))
+	  isar-keywords-proof-close))
 
 (defconst isar-keywords-indent-enclose
   (append isar-keywords-proof-block
-          isar-keywords-proof-close
-          isar-keywords-qed-block
-          (list isar-keyword-begin)))
+	  isar-keywords-proof-close
+	  isar-keywords-qed-block
+	  (list isar-keyword-begin)))
 
 
 ;; ----- regular expressions
@@ -173,9 +173,9 @@ This list is in the right format for proof-easy-config.")
 (defun isar-ids-to-regexp (l)
   "Maps a non-empty list of tokens `l' to a regexp matching all elements"
   (let* ((special (remove-if-not (lambda (s) (string-match "{\\|}" s)) l))
-         (normal (remove-if (lambda (s) (string-match "{\\|}" s)) l))
-         (s-reg (isar-regexp-simple-alt special))
-         (n-reg (concat "\\<\\(?:" (isar-regexp-simple-alt normal) "\\)\\>")))
+	 (normal (remove-if (lambda (s) (string-match "{\\|}" s)) l))
+	 (s-reg (isar-regexp-simple-alt special))
+	 (n-reg (concat "\\<\\(?:" (isar-regexp-simple-alt normal) "\\)\\>")))
     (cond
      ((null special) n-reg)
      ((null normal) s-reg)
@@ -258,12 +258,12 @@ matches contents of quotes for quoted identifiers.")
 		     (looking-at "[ \t\n]*--")
 		     'comment))))
       sc)))
-	  
+
 
 ;; antiquotations
 
-(defconst isar-antiq-regexp 
-  (concat "@{\\(?:[^\"{}]\\|" isar-string "\\)*}") 
+(defconst isar-antiq-regexp
+  (concat "@{\\(?:[^\"{}]\\|" isar-string "\\)*}")
   "Regexp matching Isabelle/Isar antiquotations.")
 
 ;; keyword nesting
@@ -277,10 +277,10 @@ matches contents of quotes for quoted identifiers.")
     (save-excursion
       (goto-char (point-min))
       (while (proof-re-search-forward isar-nesting-regexp limit t)
-        (cond
-         ((proof-buffer-syntactic-context))
-         ((equal (match-string 0) isar-keyword-begin) (incf nesting))
-         ((equal (match-string 0) isar-keyword-end) (decf nesting)))))
+	(cond
+	 ((proof-buffer-syntactic-context))
+	 ((equal (match-string 0) isar-keyword-begin) (incf nesting))
+	 ((equal (match-string 0) isar-keyword-end) (decf nesting)))))
     nesting))
 
 (defun isar-match-nesting (limit)
@@ -364,9 +364,9 @@ matches contents of quotes for quoted identifiers.")
    (cons isar-improper-regexp 'font-lock-reference-face)
    (cons isar-antiq-regexp '(0 'font-lock-variable-name-face t))))
 
-(put 'isar-goals-mode 
+(put 'isar-goals-mode
      'font-lock-extra-managed-props '(invisible sendback))
-(put 'isar-response-mode 
+(put 'isar-response-mode
      'font-lock-extra-managed-props '(invisible sendback))
 
 (defun isar-output-flkprops (start regexp end props)
@@ -381,31 +381,31 @@ matches contents of quotes for quoted identifiers.")
 (defvar isar-output-font-lock-keywords-1
   (list
    '("\^A[IJKLMNOPV]" (0 '(face nil invisible t) t))
-   (isar-output-flkprops 
-    "\^AW" "\\(?:[^\^A]\\|\^A[^X]\\)*" "\^AX" 
+   (isar-output-flkprops
+    "\^AW" "\\(?:[^\^A]\\|\^A[^X]\\)*" "\^AX"
     '(face (:underline t) mouse-face 'highlight sendback t))
 
-   (isar-output-flk "\^A0" 
-		    "\\(?:[^\^A]\\|\^A[^1]\\)*" "\^A1" 
+   (isar-output-flk "\^A0"
+		    "\\(?:[^\^A]\\|\^A[^1]\\)*" "\^A1"
 		    'proof-warning-face)
 
 ;; done generically at the moment:
 ;; (isar-output-flk "\^AM" "\\(?:[^\^A]\\|\^A[^N]\\)*" "\^AN" 'proof-error-face)
 
-   (isar-output-flk "\^AB" isar-long-id-stuff 
+   (isar-output-flk "\^AB" isar-long-id-stuff
 		    "\^AA" 'isabelle-class-name-face)
-   (isar-output-flk "\^AC" (concat "'" isar-id) 
+   (isar-output-flk "\^AC" (concat "'" isar-id)
 		    "\^AA" 'isabelle-tfree-name-face)
    (isar-output-flk "\^AD" (concat "\\??'" isar-idx)
 		    "\^AA" 'isabelle-tvar-name-face)
    (isar-output-flk "\^AE" isar-id "\^AA" 'isabelle-free-name-face)
    (isar-output-flk "\^AF" isar-id "\^AA" 'isabelle-bound-name-face)
-   (isar-output-flk "\^AG" (concat "\\??" isar-idx) 
+   (isar-output-flk "\^AG" (concat "\\??" isar-idx)
 		    "\^AA" 'isabelle-var-name-face)
    (isar-output-flk "\^AH" (concat "\\??" isar-idx)
 		    "\^AA" 'proof-declaration-name-face)
 
-   ;; may alternatively hide the spurious ASCII characters which 
+   ;; may alternatively hide the spurious ASCII characters which
    ;; aren't needed when working in colour (Isabelle printing switch
    ;; allows this for ?'s but not for 's):
    ; (isar-output-flk "\^AC'" isar-id "\^AA" 'isabelle-tfree-name-face)
@@ -468,8 +468,8 @@ matches contents of quotes for quoted identifiers.")
 
 (defconst isar-undo-commands
   (list
-   isar-linear-undo 
-   isar-undo 
+   isar-linear-undo
+   isar-undo
    "init_toplevel" "kill_thy"
    "undos_proof"
    "cannot_undo"))
@@ -478,7 +478,7 @@ matches contents of quotes for quoted identifiers.")
   (proof-anchor-regexp
    (isar-ids-to-regexp
     (append isar-keywords-theory-begin
-            isar-keywords-theory-switch))))
+	    isar-keywords-theory-switch))))
 
 (defconst isar-end-regexp
   (proof-anchor-regexp
@@ -504,20 +504,20 @@ matches contents of quotes for quoted identifiers.")
 
 (defconst isar-any-entity-regexp
   (concat "\\(?:" (isar-ids-to-regexp isar-keywords-fume) "\\)"
-          "\\(?:\\s-*(\\s-*in[^)]+)\\)?"
-          "\\(?:" isar-name-regexp "[[:=]\\)"))
+	  "\\(?:\\s-*(\\s-*in[^)]+)\\)?"
+	  "\\(?:" isar-name-regexp "[[:=]\\)"))
 
 (defconst isar-named-entity-regexp
   (concat "\\(" (isar-ids-to-regexp isar-keywords-fume) "\\)"
-          "\\(?:\\s-*(\\s-*in[^)]+)\\)?"
-          isar-name-regexp "[[:=]" ))
+	  "\\(?:\\s-*(\\s-*in[^)]+)\\)?"
+	  isar-name-regexp "[[:=]" ))
 
 (defconst isar-unnamed-entity-regexp
   (concat "\\(" (isar-ids-to-regexp isar-keywords-fume) "\\)"))
 
 (defconst isar-next-entity-regexps
   (list isar-any-entity-regexp
-        (list isar-named-entity-regexp '(1 3))))
+	(list isar-named-entity-regexp '(1 3))))
 ;; da: I've removed unnamed entities, they clutter the menu
 ;; NB: to add back, need ? at end of isar-any-entity-regexp
 ;;      (list isar-unnamed-entity-regexp 1)))
@@ -525,12 +525,12 @@ matches contents of quotes for quoted identifiers.")
 
 (defconst isar-generic-expression
   (mapcar (lambda (kw)
-            (list (capitalize kw)
-                  (concat "\\<" kw "\\>"
-                          "\\(?:\\s-*(\\s-*in[^)]+)\\)?"
-                          isar-name-regexp "[[:=]")
-                  1))
-          isar-keywords-fume))
+	    (list (capitalize kw)
+		  (concat "\\<" kw "\\>"
+			  "\\(?:\\s-*(\\s-*in[^)]+)\\)?"
+			  isar-name-regexp "[[:=]")
+		  1))
+	  isar-keywords-fume))
 
 ;; ----- indentation