--- a/src/HOL/Codatatype/Tools/bnf_tactics.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML Fri Sep 21 15:53:29 2012 +0200
@@ -16,8 +16,8 @@
val subst_asm_tac: Proof.context -> thm list -> int -> tactic
val subst_tac: Proof.context -> thm list -> int -> tactic
val substs_tac: Proof.context -> thm list -> int -> tactic
- val unfold_defs_tac: Proof.context -> thm list -> tactic
- val mk_unfold_defs_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic
+ val unfold_thms_tac: Proof.context -> thm list -> tactic
+ val mk_unfold_thms_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic
val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic
val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list ->
@@ -57,11 +57,11 @@
rtac (Drule.instantiate_normalize insts thm) 1
end);
-fun unfold_defs_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
+fun unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
-fun mk_unfold_defs_then_tac lthy defs tac x = unfold_defs_tac lthy defs THEN tac x;
+fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x;
-(*unlike "unfold_defs_tac", succeeds when the RHS contains schematic variables not in the LHS*)
+(*unlike "unfold_thms_tac", succeeds when the RHS contains schematic variables not in the LHS*)
fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt [0];
fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt [0];
fun substs_tac ctxt = REPEAT_DETERM oo subst_tac ctxt;
@@ -99,13 +99,13 @@
end;
fun simple_rel_O_Gr_tac ctxt =
- unfold_defs_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1;
+ unfold_thms_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1;
fun mk_pred_simp_tac rel_def IJpred_defs IJrel_defs rel_simp {context = ctxt, prems = _} =
- unfold_defs_tac ctxt IJpred_defs THEN
- subst_tac ctxt [unfold_defs ctxt (IJpred_defs @ IJrel_defs @
+ unfold_thms_tac ctxt IJpred_defs THEN
+ subst_tac ctxt [unfold_thms ctxt (IJpred_defs @ IJrel_defs @
@{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) rel_simp] 1 THEN
- unfold_defs_tac ctxt (rel_def ::
+ unfold_thms_tac ctxt (rel_def ::
@{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv
split_conv}) THEN
rtac refl 1;