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