# HG changeset patch
# User berghofe
# Date 1206026903 -3600
# Node ID cb6f360ab425ce538479d4c4b6fd5d0a2dac1848
# Parent  9d95309f806954ca166c0ccdcc5cd6ae1693bec4
Equivariance prover now uses permutation simprocs as well.

diff -r 9d95309f8069 -r cb6f360ab425 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 20 16:04:34 2008 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 20 16:28:23 2008 +0100
@@ -605,9 +605,10 @@
          atoms)
       end;
     val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
-    val eqvt_ss = HOL_basic_ss addsimps
+    val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss addsimps
       (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
-      [mk_perm_bool_simproc names];
+      [mk_perm_bool_simproc names,
+       NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
     val t = Logic.unvarify (concl_of raw_induct);
     val pi = Name.variant (add_term_names (t, [])) "pi";
     val ps = map (fst o HOLogic.dest_imp)