# HG changeset patch
# User wenzelm
# Date 1180905402 -7200
# Node ID dc23c062b58c297613bddb2aa704f7d861414b7e
# Parent  43553703267cb176745c03b625ea47df64472801
renamed gen_submultiset to submultiset;

diff -r 43553703267c -r dc23c062b58c src/HOL/List.thy
--- 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;