--- a/Nominal/nominal_atoms.ML	Mon Mar 29 00:30:47 2010 +0200
+++ b/Nominal/nominal_atoms.ML	Mon Mar 29 01:23:24 2010 +0200
@@ -43,11 +43,11 @@
     (* typedef *)
     val set = atom_decl_set str;
     val tac = rtac @{thm exists_eq_simple_sort} 1;
-    val ((full_tname, info as {type_definition, Rep_name, Abs_name, ...}), thy) =
+    val ((full_tname, info  as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) =
       Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy;
 
     (* definition of atom and permute *)
-    val newT = #abs_type info;
+    val newT = #abs_type (fst info);
     val RepC = Const (Rep_name, newT --> atomT);
     val AbsC = Const (Abs_name, atomT --> newT);
     val a = Free ("a", newT);