diff -r 3a8d722fd3ff -r 16c4ea954511 ex/Sorting.ML
--- a/ex/Sorting.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/ex/Sorting.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -14,13 +14,13 @@
 goal Sorting.thy "!x.mset(xs@ys,x) = mset(xs,x)+mset(ys,x)";
 by(list_ind_tac "xs" 1);
 by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if]))));
-val mset_app_distr = result();
+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(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if]))));
-val mset_compl_add = result();
+qed "mset_compl_add";
 
 val sorting_ss = sorting_ss addsimps
       [mset_app_distr, mset_compl_add];