src/HOL/ex/Sorting.ML

--- a/src/HOL/ex/Sorting.ML	Sun Nov 02 14:01:38 1997 +0100
+++ b/src/HOL/ex/Sorting.ML	Mon Nov 03 08:08:14 1997 +0100
@@ -30,7 +30,7 @@
 val prems = goalw Sorting.thy [transf_def]
   "transf(le) ==> sorted1 le xs = sorted le xs";
 by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_list_case])));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [split_list_case])));
 by (cut_facts_tac prems 1);
 by (Fast_tac 1);
 qed "sorted1_is_sorted";