1.1 --- a/src/HOL/Nominal/nominal_package.ML	Mon Oct 17 18:34:51 2005 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Mon Oct 17 19:19:29 2005 +0200
     1.3 @@ -1717,7 +1717,9 @@
     1.4                    rep_inject_thms')) 1,
     1.5                  TRY (asm_full_simp_tac (HOL_basic_ss addsimps (fresh_def :: supp_def ::
     1.6                    alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
     1.7 -                  perm_rep_perm_thms)) 1)])
     1.8 +                  perm_rep_perm_thms)) 1),
     1.9 +                TRY (asm_full_simp_tac (HOL_basic_ss addsimps (perm_fun_def ::
    1.10 +                  expand_fun_eq :: rep_inject_thms @ perm_rep_perm_thms)) 1)])
    1.11          end) (constrs ~~ constr_rep_thms)
    1.12        end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
    1.13  
    1.14 @@ -1769,7 +1771,7 @@
    1.15              (fn _ =>
    1.16                [simp_tac (HOL_basic_ss addsimps (supp_def ::
    1.17                   Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
    1.18 -                 refl :: symmetric empty_def :: Finites.emptyI :: simp_thms @
    1.19 +                 symmetric empty_def :: Finites.emptyI :: simp_thms @
    1.20                   abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1])
    1.21          in
    1.22            (supp_thm,