diff -r b93cc55cb7ab -r df6b3bd14dcb ex/Sorting.ML
--- a/ex/Sorting.ML	Fri Dec 02 11:43:20 1994 +0100
+++ b/ex/Sorting.ML	Fri Dec 02 16:09:49 1994 +0100
@@ -12,13 +12,13 @@
        Sorting.sorted1_Nil,Sorting.sorted1_One,Sorting.sorted1_Cons];
 
 goal Sorting.thy "!x.mset(xs@ys,x) = mset(xs,x)+mset(ys,x)";
-by(list_ind_tac "xs" 1);
+by(list.induct_tac "xs" 1);
 by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if]))));
 qed "mset_app_distr";
 
 goal Sorting.thy "!x. mset([x:xs. ~p(x)], x) + mset([x:xs.p(x)], x) = \
 \                     mset(xs, x)";
-by(list_ind_tac "xs" 1);
+by(list.induct_tac "xs" 1);
 by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if]))));
 qed "mset_compl_add";