Removed superfluous variable. Improved docstrings.

2 files changed, 7 insertions, 10 deletions

diff --git a/isa/isa.el b/isa/isa.el
index 06c52c47..bcbde84a 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -335,12 +335,6 @@ Resulting output from Isabelle will be parsed by Proof General."
 ;; Next portion taken from isa-load.el
 ;; isa-load.el,v 3.8 1998/09/01 
 
-(defcustom isabelle-use-sml-mode
-   (if (fboundp 'sml-mode) 'sml-mode)
-  "*If non-nil, attempt to use sml-mode in ML section of theory files."
-  :type 'boolean
-  :group 'isabelle)
-
 (defgroup thy nil
   "Customization of Isamode's theory editing mode"
   ;; :link '(info-link "(Isamode)Theory Files")
diff --git a/isa/thy-mode.el b/isa/thy-mode.el
index dd0416a8..e7932068 100644
--- a/isa/thy-mode.el
+++ b/isa/thy-mode.el
@@ -73,9 +73,12 @@ any of the usual bracket characters in unusual ways."
     ("end")
     ("ML"))
   "Names of theory file sections and their templates.
-Template is either a string to insert or a function. Useful functions are:
+Each item in the list is a pair of a section name and a template.
+A template is either a string to insert or a function. Useful functions are:
   thy-insert-header, thy-insert-class, thy-insert-default-sort,
-  thy-insert-const, thy-insert-rule"
+  thy-insert-const, thy-insert-rule.
+The nil template does nothing.
+You can add extra sections to theory files by extending this variable."
   :type '(repeat
 	  (cons string
 	       (choice function
@@ -109,8 +112,8 @@ ML\n"
 "*Template for theory files.
 Contains a default selection of sections in a traditional order.
 You can use the following format characters:
-  %t  -- replaced by theory name
-  %p  -- replaced by names of parents, separated by +'s"
+  %t --- replaced by theory name
+  %p --- replaced by names of parents, separated by +'s"
  :group 'thy
  :type 'string)