# HG changeset patch
# User berghofe
# Date 1129569569 -7200
# Node ID 8be65cf94d2e103cb8a3b0d4e6aabc23fd2b1d84
# Parent  09236f6a6a194448dc61c615ba5467be6ab1cbdc
Improved proof of injectivity theorems to make it work on
"ordinary" function types as well.

diff -r 09236f6a6a19 -r 8be65cf94d2e src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Mon Oct 17 18:34:51 2005 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Mon Oct 17 19:19:29 2005 +0200
@@ -1717,7 +1717,9 @@
                   rep_inject_thms')) 1,
                 TRY (asm_full_simp_tac (HOL_basic_ss addsimps (fresh_def :: supp_def ::
                   alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
-                  perm_rep_perm_thms)) 1)])
+                  perm_rep_perm_thms)) 1),
+                TRY (asm_full_simp_tac (HOL_basic_ss addsimps (perm_fun_def ::
+                  expand_fun_eq :: rep_inject_thms @ perm_rep_perm_thms)) 1)])
         end) (constrs ~~ constr_rep_thms)
       end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
 
@@ -1769,7 +1771,7 @@
             (fn _ =>
               [simp_tac (HOL_basic_ss addsimps (supp_def ::
                  Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
-                 refl :: symmetric empty_def :: Finites.emptyI :: simp_thms @
+                 symmetric empty_def :: Finites.emptyI :: simp_thms @
                  abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1])
         in
           (supp_thm,