1.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Nov 29 01:37:01 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Tue Nov 29 12:26:22 2005 +0100
     1.3 @@ -138,9 +138,6 @@
     1.4        (DatatypePackage.get_datatypes thy1) (hd full_new_type_names');
     1.5      fun nth_dtyp i = typ_of_dtyp descr sorts' (DtRec i);
     1.6  
     1.7 -    val dt_atomTs = filter (fn Type (s, []) => s mem atoms | _ => false)
     1.8 -      (get_nonrec_types descr sorts);
     1.9 -
    1.10      (**** define permutation functions ****)
    1.11  
    1.12      val permT = mk_permT (TFree ("'x", HOLogic.typeS));
    1.13 @@ -402,6 +399,10 @@
    1.14            apfst (cons dt) (strip_option dt')
    1.15        | strip_option dt = ([], dt);
    1.16  
    1.17 +    val dt_atomTs = distinct (map (typ_of_dtyp descr sorts')
    1.18 +      (List.concat (map (fn (_, (_, _, cs)) => List.concat
    1.19 +        (map (List.concat o map (fst o strip_option) o snd) cs)) descr)));
    1.20 +
    1.21      fun make_intr s T (cname, cargs) =
    1.22        let
    1.23          fun mk_prem (dt, (j, j', prems, ts)) =