diff -r a44479bde681 -r 017e33849f4d Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Tue Mar 22 12:18:30 2016 +0000
+++ b/Nominal/nominal_function.ML	Thu Apr 19 13:57:17 2018 +0100
@@ -12,19 +12,19 @@
   include NOMINAL_FUNCTION_DATA
 
   val add_nominal_function: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list ->  Nominal_Function_Common.nominal_function_config ->
+    Specification.multi_specs ->  Nominal_Function_Common.nominal_function_config ->
     (Proof.context -> tactic) -> local_theory -> nominal_info * local_theory
 
   val add_nominal_function_cmd: (binding * string option * mixfix) list ->
-    (Attrib.binding * string) list ->  Nominal_Function_Common.nominal_function_config ->
+    Specification.multi_specs_cmd ->  Nominal_Function_Common.nominal_function_config ->
     (Proof.context -> tactic) -> bool -> local_theory -> nominal_info * local_theory
 
   val nominal_function: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list ->  Nominal_Function_Common.nominal_function_config ->
+    Specification.multi_specs ->  Nominal_Function_Common.nominal_function_config ->
     local_theory -> Proof.state
 
   val nominal_function_cmd: (binding * string option * mixfix) list ->
-    (Attrib.binding * string) list ->  Nominal_Function_Common.nominal_function_config ->
+    Specification.multi_specs_cmd ->  Nominal_Function_Common.nominal_function_config ->
     bool -> local_theory -> Proof.state
 
   val get_info : Proof.context -> term -> nominal_info
@@ -102,7 +102,7 @@
 
 val simp_attribs = map (Attrib.internal o K)
   [Simplifier.simp_add,
-   Code.add_default_eqn_attribute,
+   Code.add_default_eqn_attribute Code.Equation,
    Named_Theorems.add @{named_theorems nitpick_simp}]
 
 val psimp_attribs = map (Attrib.internal o K)
@@ -203,9 +203,9 @@
   end
 
 val add_nominal_function =
-  gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type})
+  gen_add_nominal_function false Specification.check_multi_specs (Type_Infer.anyT @{sort type})
 fun add_nominal_function_cmd a b c d int = 
-  gen_add_nominal_function int Specification.read_spec "_::type" a b c d
+  gen_add_nominal_function int Specification.read_multi_specs "_::type" a b c d
 
 fun gen_nominal_function do_print prep default_constraint fixspec eqns config lthy =
   let
@@ -218,9 +218,9 @@
   end
 
 val nominal_function =
-  gen_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type})
+  gen_nominal_function false Specification.check_multi_specs (Type_Infer.anyT @{sort type})
 fun nominal_function_cmd a b c int = 
-  gen_nominal_function int Specification.read_spec "_::type" a b c
+  gen_nominal_function int Specification.read_multi_specs "_::type" a b c
 
 fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
   |> the_single |> snd
@@ -241,16 +241,13 @@
      >> (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
+      config_parser default_cfg -- Parse_Spec.specification
 end
 
-
-(* nominal *)
 val _ =
   Outer_Syntax.local_theory_to_proof' @{command_keyword nominal_function}
     "define general recursive nominal functions"
        (nominal_function_parser nominal_default_config
-          >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config))
-
+          >> (fn (config, (fixes, specs)) => nominal_function_cmd fixes specs config))
 
 end