--- a/Nominal/nominal_dt_supp.ML	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/nominal_dt_supp.ML	Wed Nov 10 13:46:21 2010 +0000
@@ -144,7 +144,7 @@
 
 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc}
 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un}
-val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def 
+val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def 
   prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] Finite_Set.finite.emptyI}
 
 fun p_tac msg i =