# HG changeset patch
# User nipkow
# Date 1458301680 -3600
# Node ID 66568c9b82163a711c28d48c625ba240ae26e66c
# Parent  7e6bb43e72178175e4dba1a742c7ee9b216490d5
superfluous premise (noticed by Julian Nagele)

diff -r 7e6bb43e7217 -r 66568c9b8216 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Mar 18 10:14:56 2016 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Mar 18 12:48:00 2016 +0100
@@ -2062,7 +2062,7 @@
 done
 
 lemma one_step_implies_mult:
-  "trans r \<Longrightarrow> J \<noteq> {#} \<Longrightarrow> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r
+  "J \<noteq> {#} \<Longrightarrow> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r
     \<Longrightarrow> (I + K, I + J) \<in> mult r"
 using one_step_implies_mult_aux by blast
 
diff -r 7e6bb43e7217 -r 66568c9b8216 src/HOL/ZF/LProd.thy
--- a/src/HOL/ZF/LProd.thy	Fri Mar 18 10:14:56 2016 +0100
+++ b/src/HOL/ZF/LProd.thy	Fri Mar 18 12:48:00 2016 +0100
@@ -59,7 +59,7 @@
   proof (cases "a = b")
     case True    
     have "((I + {#b#}) + K, (I + {#b#}) + J) \<in> mult R"
-      apply (rule one_step_implies_mult[OF transR])
+      apply (rule one_step_implies_mult)
       apply (auto simp add: decomposed)
       done
     then show ?thesis
@@ -71,7 +71,7 @@
     case False
     from False lprod_list have False: "(a, b) \<in> R" by blast
     have "(I + (K + {#a#}), I + (J + {#b#})) \<in> mult R"
-      apply (rule one_step_implies_mult[OF transR])
+      apply (rule one_step_implies_mult)
       apply (auto simp add: False decomposed)
       done
     then show ?thesis