renamed gen_submultiset to submultiset;
authorwenzelm
Sun, 03 Jun 2007 23:16:42 +0200
changeset 23214 dc23c062b58c
parent 23213 43553703267c
child 23215 20b5558a5419
renamed gen_submultiset to submultiset;
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;