doc-src/IsarRef/Thy/HOL_Specific.thy

     @{command_def (HOL) "fun"} & : & \isarkeep{local{\dsh}theory} \\
     @{command_def (HOL) "function"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
     @{command_def (HOL) "termination"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
   \end{matharray}
 
-  \railalias{funopts}{function\_opts}  %FIXME ??
-
   \begin{rail}
     'primrec' target? fixes 'where' equations
     ;
     equations: (thmdecl? prop + '|')
     ;
-    ('fun' | 'function') (funopts)? fixes 'where' clauses
+    ('fun' | 'function') target? functionopts? fixes 'where' clauses
     ;
     clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
     ;
-    funopts: '(' (('sequential' | 'in' name | 'domintros' | 'tailrec' |
-    'default' term) + ',') ')'
+    functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
     ;
     'termination' ( term )?
   \end{rail}
 
   \begin{descr}

   programming.  Note that the resulting simplification and induction
   rules correspond to the transformed specification, not the one given
   originally. This usually means that each equation given by the user
   may result in several theroems.  Also note that this automatic
   transformation only works for ML-style datatype patterns.
-
-  \item [@{text "\<IN> name"}] gives the target for the definition.
-  %FIXME ?!?
 
   \item [@{text domintros}] enables the automated generation of
   introduction rules for the domain predicate. While mostly not
   needed, they can be helpful in some proofs about partial functions.