# HG changeset patch
# User traytel
# Date 1376330643 -7200
# Node ID 7f7bbeb165382cf79b0581517c2c389ad8f73c31
# Parent  9e22d62642776ae41c80c1cc189c7186788644b0
eliminated bogus assumption from theorem (that was instantiated with refl and resulted in flexflex pairs)

diff -r 9e22d6264277 -r 7f7bbeb16538 src/HOL/BNF/BNF_Def.thy
--- 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
diff -r 9e22d6264277 -r 7f7bbeb16538 src/HOL/BNF/Tools/bnf_def_tactics.ML
--- 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;