src/HOL/Library/Multiset.thy
changeset 33102 e3463e6db704
parent 32960 69916a850301
child 34943 e97b22500a5c
--- a/src/HOL/Library/Multiset.thy	Sat Oct 24 20:47:10 2009 +0200
+++ b/src/HOL/Library/Multiset.thy	Sun Oct 25 00:00:53 2009 +0200
@@ -1607,7 +1607,7 @@
       rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
 
   val regroup_munion_conv =
-      FundefLib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus}
+      Function_Lib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus}
         (map (fn t => t RS eq_reflection) (@{thms union_ac} @ @{thms empty_idemp}))
 
   fun unfold_pwleq_tac i =