src/HOL/Lex/MaxChop.ML

--- a/src/HOL/Lex/MaxChop.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/MaxChop.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -84,7 +84,7 @@
                         addsplits [split_split]) 1);
 by (Clarify_tac 1);
 by (rename_tac "xs1 ys1 xss1 ys" 1);
-by (split_asm_tac [split_list_case_asm] 1);
+by (split_asm_tac [list.split_asm] 1);
  by (Asm_full_simp_tac 1);
  by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
  by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);