src/HOL/Nominal/nominal_permeq.ML
changeset 22610 c8b5133045f3
parent 22609 40ade470e319
child 22656 13302b2d0948
     1.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Sat Apr 07 11:05:25 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Apr 07 11:36:35 2007 +0200
     1.3 @@ -71,7 +71,6 @@
     1.4  fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) (Name name);
     1.5  fun dynamic_thm  st name = PureThy.get_thm  (theory_of_thm st) (Name name);
     1.6  
     1.7 -fun eqvts_thms st = NominalThmDecls.get_eqvt_thms (theory_of_thm st);
     1.8  
     1.9  (* needed in the process of fully simplifying permutations *)
    1.10  val strong_congs = [thm "if_cong"]
    1.11 @@ -153,8 +152,18 @@
    1.12      end);
    1.13  
    1.14  (* general simplification of permutations and permutation that arose from eqvt-problems *)
    1.15 -val perm_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simp_a","swap_simp_b"] (fn st => []);
    1.16 -val eqvt_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_pi_simp"] eqvts_thms;
    1.17 +val perm_simp = 
    1.18 +    let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"]
    1.19 +    in 
    1.20 +	perm_simp_gen simps (fn st => [])
    1.21 +    end;
    1.22 +
    1.23 +val eqvt_simp = 
    1.24 +    let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"]
    1.25 +	fun eqvts_thms st = NominalThmDecls.get_eqvt_thms (theory_of_thm st);
    1.26 +    in 
    1.27 +	perm_simp_gen simps eqvts_thms
    1.28 +    end;
    1.29  
    1.30  (* FIXME removes the name lookup for these theorems use an ml value instead *)
    1.31