src/HOL/List.thy

 lemma lexn_length:
   "(xs, ys) \<in> lexn r n \<Longrightarrow> length xs = n \<and> length ys = n"
 by (induct n arbitrary: xs ys) auto
 
 lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
-apply (unfold lex_def)
-apply (rule wf_UN)
-apply (blast intro: wf_lexn, clarify)
-apply (rename_tac m n)
-apply (subgoal_tac "m \<noteq> n")
- prefer 2 apply blast
-apply (blast dest: lexn_length not_sym)
-done
+  apply (unfold lex_def)
+  apply (rule wf_UN)
+   apply (simp add: wf_lexn)
+  apply (metis DomainE Int_emptyI RangeE lexn_length)
+  done
 
 lemma lexn_conv:
   "lexn r n =
     {(xs,ys). length xs = n \<and> length ys = n \<and>
     (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y) \<in> r)}"