diff -r c3ff26204d2a -r d29a8a6f3138 Nominal/nominal_inductive.ML --- a/Nominal/nominal_inductive.ML Thu Apr 28 11:44:36 2011 +0800 +++ b/Nominal/nominal_inductive.ML Thu Apr 28 11:51:01 2011 +0800 @@ -139,10 +139,10 @@ in (* by default eqvt_strict_config contains unwanted @{thm permute_pure} *) -val eqvt_sconfig = (delposts eqvt_strict_config) addpres @{thms permute_minus_cancel} +val eqvt_sconfig = eqvt_strict_config addpres @{thms permute_minus_cancel} fun eqvt_stac ctxt = eqvt_tac ctxt eqvt_sconfig -fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig +fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig end @@ -175,7 +175,9 @@ val prm_tys = map (fastype_of o term_of) prms val cperms = map (cterm_of thy o perm_const) prm_tys val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms - val prem' = cterm_instantiate (intr_cvars ~~ p_prms) prem + val prem' = prem + |> cterm_instantiate (intr_cvars ~~ p_prms) + |> eqvt_srule ctxt (* for inductive-premises*) fun tac1 prm = helper_tac true prm p context @@ -189,7 +191,9 @@ fun select prm (t, i) = (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i in - EVERY1 [eqvt_stac ctxt, rtac prem', RANGE (map (SUBGOAL o select) prems) ] + EVERY1 [ eqvt_stac context, + rtac prem', + RANGE (map (SUBGOAL o select) prems) ] end) ctxt fun fresh_thm ctxt user_thm p c concl_args avoid_trm = @@ -244,7 +248,9 @@ val cperms = map (cterm_of thy o perm_const) prm_tys val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms - val prem' = cterm_instantiate (intr_cvars ~~ qp_prms) prem + val prem' = prem + |> cterm_instantiate (intr_cvars ~~ qp_prms) + |> eqvt_srule ctxt val fprop' = eqvt_srule ctxt' fprop val tac_fresh = simp_tac (HOL_basic_ss addsimps [fprop']) @@ -277,7 +283,8 @@ val tac1 = non_binder_tac prem intr_cvars Ps ctxt val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt in - EVERY' [ rtac @{thm allI}, rtac @{thm allI}, if null avoid then tac1 else tac2 ] + EVERY' [ rtac @{thm allI}, rtac @{thm allI}, + if null avoid then tac1 else tac2 ] end fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args