Equivariance prover now uses permutation simprocs as well.
authorberghofe
Thu Mar 20 16:28:23 2008 +0100 (2008-03-20 ago)
changeset 26364cb6f360ab425
parent 26363 9d95309f8069
child 26365 e6d3714b8853
Equivariance prover now uses permutation simprocs as well.
src/HOL/Nominal/nominal_inductive.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 20 16:04:34 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 20 16:28:23 2008 +0100
     1.3 @@ -605,9 +605,10 @@
     1.4           atoms)
     1.5        end;
     1.6      val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
     1.7 -    val eqvt_ss = HOL_basic_ss addsimps
     1.8 +    val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss addsimps
     1.9        (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
    1.10 -      [mk_perm_bool_simproc names];
    1.11 +      [mk_perm_bool_simproc names,
    1.12 +       NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
    1.13      val t = Logic.unvarify (concl_of raw_induct);
    1.14      val pi = Name.variant (add_term_names (t, [])) "pi";
    1.15      val ps = map (fst o HOLogic.dest_imp)