--- a/Nominal/nominal_atoms.ML	Tue Mar 22 12:18:30 2016 +0000
+++ b/Nominal/nominal_atoms.ML	Thu Apr 19 13:57:17 2018 +0100
@@ -58,9 +58,9 @@
     val lthy =
       Class.instantiation ([full_tname], [], @{sort at}) thy;
     val ((_, (_, permute_ldef)), lthy) =
-      Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy;
+      Specification.definition NONE [] [] ((permute_def_name, []), permute_eqn) lthy;
     val ((_, (_, atom_ldef)), lthy) =
-      Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy;
+      Specification.definition NONE [] [] ((atom_def_name, []), atom_eqn) lthy;
     val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy);
     val permute_def = singleton (Proof_Context.export lthy ctxt_thy) permute_ldef;
     val atom_def = singleton (Proof_Context.export lthy ctxt_thy) atom_ldef;