--- a/Nominal/nominal_function.ML	Sun Jun 05 16:58:18 2011 +0100
+++ b/Nominal/nominal_function.ML	Sun Jun 05 21:14:23 2011 +0100
@@ -12,19 +12,19 @@
   include FUNCTION_DATA
 
   val add_nominal_function: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list -> Function_Common.function_config ->
+    (Attrib.binding * term) list ->  Nominal_Function_Common.nominal_function_config ->
     (Proof.context -> tactic) -> local_theory -> info * local_theory
 
   val add_nominal_function_cmd: (binding * string option * mixfix) list ->
-    (Attrib.binding * string) list -> Function_Common.function_config ->
+    (Attrib.binding * string) list ->  Nominal_Function_Common.nominal_function_config ->
     (Proof.context -> tactic) -> local_theory -> info * local_theory
 
   val nominal_function: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list -> Function_Common.function_config ->
+    (Attrib.binding * term) list ->  Nominal_Function_Common.nominal_function_config ->
     local_theory -> Proof.state
 
   val nominal_function_cmd: (binding * string option * mixfix) list ->
-    (Attrib.binding * string) list -> Function_Common.function_config ->
+    (Attrib.binding * string) list ->  Nominal_Function_Common.nominal_function_config ->
     local_theory -> Proof.state
 
   val setup : theory -> theory
@@ -38,8 +38,7 @@
 struct
 
 open Function_Lib
-open Function_Common
-
+open Nominal_Function_Common
 
 
 (* Check for all sorts of errors in the input - nominal needs a different checking function *)
@@ -144,7 +143,7 @@
       empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *)
 
     val defname = mk_defname fixes
-    val FunctionConfig {partials, default, ...} = config
+    val NominalFunctionConfig {partials, default, ...} = config
     val _ =
       if is_some default then Output.legacy_feature
         "'function (default)'. Use 'partial_function'."
@@ -257,11 +256,28 @@
 
 (* outer syntax *)
 
+local
+  val option_parser = Parse.group "option"
+    ((Parse.reserved "sequential" >> K Sequential)
+     || ((Parse.reserved "default" |-- Parse.term) >> Default)
+     || (Parse.reserved "domintros" >> K DomIntros)
+     || (Parse.reserved "no_partials" >> K No_Partials)
+     || ((Parse.reserved "invariant" |-- Parse.term) >> Invariant))
+
+  fun config_parser default =
+    (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
+     >> (fn opts => fold apply_opt opts default)
+in
+  fun nominal_function_parser default_cfg =
+      config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
+end
+
+
 (* nominal *)
 val _ =
   Outer_Syntax.local_theory_to_proof "nominal_primrec" "define general recursive nominal functions"
   Keyword.thy_goal
-  (function_parser default_config
+  (nominal_function_parser nominal_default_config
      >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config))