src/HOL/ex/Sorting.ML
changeset 3465 e85c24717cad
parent 2517 2af078382853
child 3647 a64c8fbcd98f
--- a/src/HOL/ex/Sorting.ML	Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/ex/Sorting.ML	Thu Jun 26 13:20:50 1997 +0200
@@ -19,7 +19,7 @@
 
 Addsimps [mset_append, mset_compl_add];
 
-goal Sorting.thy "set_of_list xs = {x.mset xs x ~= 0}";
+goal Sorting.thy "set xs = {x.mset xs x ~= 0}";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 by (Fast_tac 1);