--- 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)) =