diff -r 653c84d5c6c9 -r 43a5b86bc102 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Dec 13 20:29:59 2011 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Dec 13 23:23:51 2011 +0100
@@ -99,7 +99,7 @@
     
     val (_,thy1) = 
     fold_map (fn ak => fn thy => 
-          let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
+          let val dt = ((Binding.name ak, [], NoSyn), [(Binding.name ak, [@{typ nat}], NoSyn)])
               val (dt_names, thy1) = Datatype.add_datatype Datatype.default_config [dt] thy;
             
               val injects = maps (#inject o Datatype.the_info thy1) dt_names;