eliminated bogus assumption from theorem (that was instantiated with refl and resulted in flexflex pairs)

--- a/src/HOL/BNF/BNF_Def.thy	Mon Aug 12 15:36:55 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy	Mon Aug 12 20:04:03 2013 +0200
@@ -31,7 +31,7 @@
 unfolding convol_def by simp
 
 lemma convol_mem_GrpI:
-"\<lbrakk>g x = g' x; x \<in> A\<rbrakk> \<Longrightarrow> <id , g> x \<in> (Collect (split (Grp A g)))"
+"x \<in> A \<Longrightarrow> <id , g> x \<in> (Collect (split (Grp A g)))"
 unfolding convol_def Grp_def by auto
 
 definition csquare where

--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Mon Aug 12 15:36:55 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Mon Aug 12 20:04:03 2013 +0200
@@ -111,7 +111,7 @@
             rtac CollectI,
             CONJ_WRAP' (fn thm =>
               EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
-                rtac @{thm convol_mem_GrpI[OF refl]}, etac set_mp, atac])
+                rtac @{thm convol_mem_GrpI}, etac set_mp, atac])
             set_maps])
           @{thms fst_convol snd_convol} [map_id', refl])] 1
   end;