src/HOL/List.thy
changeset 23214 dc23c062b58c
parent 23212 82881b1ae9c6
child 23235 eb365b39b36d
--- a/src/HOL/List.thy	Sun Jun 03 23:16:41 2007 +0200
+++ b/src/HOL/List.thy	Sun Jun 03 23:16:42 2007 +0200
@@ -381,8 +381,8 @@
           (K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1));
       in SOME (thm RS @{thm neq_if_length_neq}) end
   in
-    if m < n andalso gen_submultiset (op aconv) (ls,rs) orelse
-       n < m andalso gen_submultiset (op aconv) (rs,ls)
+    if m < n andalso submultiset (op aconv) (ls,rs) orelse
+       n < m andalso submultiset (op aconv) (rs,ls)
     then prove_neq() else NONE
   end;