added nonterminals, setup;
removed print_data;

--- a/doc-src/Ref/theories.tex	Mon Aug 24 18:17:25 1998 +0200
+++ b/doc-src/Ref/theories.tex	Mon Aug 24 18:58:12 1998 +0200
@@ -82,6 +82,10 @@
   arities to type constructors.  The $name$ must be an existing type
   constructor, which is given the additional arity $arity$.
   
+\item[$nonterminals$]\index{*nonterminal symbols} declares purely
+  syntactic types to be used as nonterminal symbols of the context
+  free grammar.
+
 \item[$consts$] is a series of constant declarations.  Each new
   constant $name$ is given the specified type.  The optional $mixfix$
   annotations may attach concrete syntax to the constant.
@@ -147,7 +151,7 @@
   allowed to create theorems, but each theorem carries a proof object
   describing the oracle invocation.  See \S\ref{sec:oracles} for details.
   
-\item[$local, global$] changes the current name declaration mode.
+\item[$local$, $global$] change the current name declaration mode.
   Initially, theories start in $local$ mode, causing all names of
   types, constants, axioms etc.\ to be automatically qualified by the
   theory name.  Changing this to $global$ causes all names to be
@@ -158,6 +162,11 @@
   note that the final state at the end of the theory will persist.  In
   particular, this determines how the names of theorems stored later
   on are handled.
+  
+\item[$setup$]\index{*setup!theory} applies a list of ML functions to
+  the theory.  The argument should denote a value of type
+  \texttt{(theory -> theory) list}.  Typically, ML packages are
+  initialized in this way.
 
 \item[$ml$] \index{*ML section}
   consists of \ML\ code, typically for parse and print translation functions.
@@ -529,7 +538,6 @@
 \begin{ttbox}
 print_syntax        : theory -> unit
 print_theory        : theory -> unit
-print_data          : theory -> string -> unit
 parents_of          : theory -> theory list
 ancestors_of        : theory -> theory list
 sign_of             : theory -> Sign.sg
@@ -544,11 +552,6 @@
 \item[\ttindexbold{print_theory} $thy$] prints the logical parts of
   $thy$, excluding the syntax.
   
-\item[\ttindexbold{print_data} $thy$ $kind$] prints generic data of
-  $thy$.  This invokes the print method associated with $kind$.  Refer
-  to the output of \texttt{print_theory} for a list of available data
-  kinds in $thy$.
-  
 \item[\ttindexbold{parents_of} $thy$] returns the direct ancestors
   of~$thy$.
   
@@ -930,3 +933,9 @@
 
 \index{oracles|)}
 \index{theories|)}
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "ref"
+%%% End: 

--- a/doc-src/Ref/theory-syntax.tex	Mon Aug 24 18:17:25 1998 +0200
+++ b/doc-src/Ref/theory-syntax.tex	Mon Aug 24 18:58:12 1998 +0200
@@ -32,8 +32,8 @@
 theoryDef : id '=' (name + '+') ('+' extension | ())
           ;
 
-name: id | string
-    ;
+name : id | string
+     ;
 
 extension : (section +) 'end' ( () | ml )
           ;
@@ -42,6 +42,7 @@
         | default
         | types
         | arities
+        | nonterminals
         | consts
         | syntax
         | trans
@@ -53,13 +54,14 @@
         | oracle
         | local
         | global
+        | setup
         ;
 
 classes : 'classes' ( classDecl + )
         ;
 
 classDecl : (id (() | '<' (id + ',')))
-        ;
+          ;
 
 default : 'default' sort 
         ;
@@ -92,6 +94,9 @@
 arity : ( () | '(' (sort + ',') ')' ) sort
       ;
 
+nonterminals : 'nonterminals' (name+)
+             ;
+
 consts : 'consts' ( mixfixConstDecl + )
        ;
 
@@ -129,19 +134,28 @@
 instance : 'instance' ( name '<' name | name '::' arity) witness
          ;
 
-witness : (() | '(' ((string | longident) + ',') ')') (() | verbatim)
+witness : (() | '(' ((string | id | longident) + ',') ')') (() | verbatim)
         ;
 
 oracle : 'oracle' name '=' name
        ;
 
 local : 'local'
-       ;
+      ;
 
 global : 'global'
        ;
 
+setup : 'setup' (id | longident)
+      ;
+
 ml : 'ML' text
    ;
 
 \end{rail}
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "ref"
+%%% End: