# HG changeset patch
# User wenzelm
# Date 1150139890 -7200
# Node ID 6e44610bdd761f5bf56720c9670a728e7fd738b0
# Parent  e5c12b5cb9403cbca8125bb758649aee055be54b
fixed subst step;

diff -r e5c12b5cb940 -r 6e44610bdd76 src/HOL/ex/MergeSort.thy
--- a/src/HOL/ex/MergeSort.thy	Mon Jun 12 20:58:25 2006 +0200
+++ b/src/HOL/ex/MergeSort.thy	Mon Jun 12 21:18:10 2006 +0200
@@ -51,7 +51,7 @@
 theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
 apply (induct xs rule: msort.induct)
   apply simp_all
-apply (subst union_commute)
+apply (subst union_commute) back
 apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
 apply (simp add: union_ac)
 done