# HG changeset patch
# User paulson
# Date 953544722 -3600
# Node ID 209eb2db72e6cd964525938b4893470241aecd40
# Parent  f990040535c9494877e22f0479e89103ea82af22
renamed a variable to avoid possible free/bound confusion

diff -r f990040535c9 -r 209eb2db72e6 src/HOL/ex/Sorting.ML
--- a/src/HOL/ex/Sorting.ML	Mon Mar 20 10:26:34 2000 +0100
+++ b/src/HOL/ex/Sorting.ML	Mon Mar 20 10:32:02 2000 +0100
@@ -11,7 +11,7 @@
 by Auto_tac;
 qed "multiset_append";
 
-Goal "multiset [x:xs. ~p(x)] x + multiset [x:xs. p(x)] x = multiset xs x";
+Goal "multiset [x:xs. ~p(x)] z + multiset [x:xs. p(x)] z = multiset xs z";
 by (induct_tac "xs" 1);
 by Auto_tac;
 qed "multiset_compl_add";