diff -r f7a18e2b10fc -r 45e139675daf src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Tue Nov 29 01:37:01 2005 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Tue Nov 29 12:26:22 2005 +0100
@@ -138,9 +138,6 @@
       (DatatypePackage.get_datatypes thy1) (hd full_new_type_names');
     fun nth_dtyp i = typ_of_dtyp descr sorts' (DtRec i);
 
-    val dt_atomTs = filter (fn Type (s, []) => s mem atoms | _ => false)
-      (get_nonrec_types descr sorts);
-
     (**** define permutation functions ****)
 
     val permT = mk_permT (TFree ("'x", HOLogic.typeS));
@@ -402,6 +399,10 @@
           apfst (cons dt) (strip_option dt')
       | strip_option dt = ([], dt);
 
+    val dt_atomTs = distinct (map (typ_of_dtyp descr sorts')
+      (List.concat (map (fn (_, (_, _, cs)) => List.concat
+        (map (List.concat o map (fst o strip_option) o snd) cs)) descr)));
+
     fun make_intr s T (cname, cargs) =
       let
         fun mk_prem (dt, (j, j', prems, ts)) =