renamed a variable to avoid possible free/bound confusion
authorpaulson
Mon, 20 Mar 2000 10:32:02 +0100
changeset 8525 209eb2db72e6
parent 8524 f990040535c9
child 8526 0be2c98f15a7
renamed a variable to avoid possible free/bound confusion
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";