--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Sep 27 18:01:33 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Sep 27 18:25:41 2012 +0200
@@ -106,11 +106,10 @@
fun mk_srel_Id_tac n srel_Gr map_id {context = ctxt, prems = _} =
unfold_thms_tac ctxt [srel_Gr, @{thm Id_alt}] THEN
- subst_tac ctxt NONE [map_id] 1 THEN
- (if n = 0 then rtac refl 1
- else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
- rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI,
- CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac refl] 1);
+ (if n = 0 then rtac refl 1
+ else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
+ rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI,
+ CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id] 1);
fun mk_srel_mono_tac srel_O_Grs in_mono {context = ctxt, prems = _} =
unfold_thms_tac ctxt srel_O_Grs THEN