# HG changeset patch
# User traytel
# Date 1348763141 -7200
# Node ID 55cdf03e46c4f3628883df91e99c5365ebc63452
# Parent  7db3d29868814e08c2cac483de3043a3e893d848
tuned tactic

diff -r 7db3d2986881 -r 55cdf03e46c4 src/HOL/BNF/Tools/bnf_def_tactics.ML
--- 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