src/HOL/Tools/recdef_package.ML

--- a/src/HOL/Tools/recdef_package.ML	Sat May 20 23:36:53 2006 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Sat May 20 23:36:55 2006 +0200
@@ -80,7 +80,7 @@
 fun del_cong raw_thm congs =
   let
     val (c, thm) = prep_cong raw_thm;
-    val (del, rest) = Library.partition (Library.equal c o fst) congs;
+    val (del, rest) = List.partition (Library.equal c o fst) congs;
   in if null del then (warning ("No recdef congruence rule for " ^ quote c); congs) else rest end;
 
 val add_congs = foldr (uncurry add_cong);