--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Sat Sep 29 21:59:08 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Sun Sep 30 12:04:13 2012 +0200
@@ -141,9 +141,19 @@
pre_set_defss mss (unflat mss (1 upto n)) kkss)
end;
+local
+
+fun hhf_concl_conv cv ctxt ct =
+ (case Thm.term_of ct of
+ Const ("all", _) $ Abs _ => Conv.arg_conv (Conv.abs_conv (hhf_concl_conv cv o snd) ctxt) ct
+ | _ => Conv.concl_conv ~1 cv ct);
+
+in
+
fun mk_coinduct_same_ctr ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels =
hyp_subst_tac THEN'
- subst_tac ctxt (SOME [1, 2]) [ctr_def] THEN'
+ CONVERSION (hhf_concl_conv
+ (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN'
SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN'
SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels @ sum_prod_thms_rel)) THEN'
(atac ORELSE' REPEAT o etac conjE THEN'
@@ -151,6 +161,8 @@
(ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms)) THEN_MAYBE'
REPEAT o hyp_subst_tac THEN' REPEAT o rtac conjI THEN' REPEAT o rtac refl);
+end;
+
fun mk_coinduct_distinct_ctrs discs discs' =
hyp_subst_tac THEN' REPEAT o etac conjE THEN'
full_simp_tac (ss_only (refl :: no_refl (discs @ discs') @ basic_simp_thms));