# HG changeset patch
# User dixon
# Date 1150206172 -7200
# Node ID 1b53b196f85f0675d7d17985cd0fb474759996e5
# Parent  88e8f6173bab903682b00090e8bacbe4b7cbd434
corrected w.r.t. search order for subst.

diff -r 88e8f6173bab -r 1b53b196f85f src/HOL/ex/MergeSort.thy
--- a/src/HOL/ex/MergeSort.thy	Tue Jun 13 15:42:19 2006 +0200
+++ b/src/HOL/ex/MergeSort.thy	Tue Jun 13 15:42:52 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) back
+apply (subst union_commute)
 apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
 apply (simp add: union_ac)
 done