changeset 14401 | 477380c74c1d |
parent 10338 | 291ce4c4b50e |
--- a/src/HOL/Lex/MaxChop.ML Thu Feb 19 17:57:54 2004 +0100 +++ b/src/HOL/Lex/MaxChop.ML Thu Feb 19 18:24:08 2004 +0100 @@ -80,7 +80,7 @@ addsplits [split_split]) 1); by (Clarify_tac 1); by (rename_tac "xs1 ys1 xss1 ys" 1); -by (split_asm_tac [list.split_asm] 1); +by (split_asm_tac [thm "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 [thm "prefix_append" RS iffD2]) 1);