# HG changeset patch
# User wenzelm
# Date 1148161015 -7200
# Node ID 83611262823ed92b6e5171931e716b04be2225dc
# Parent  4477003648cc4d3626e2e08fc42aa8dbd1cb544f
List.partition;

diff -r 4477003648cc -r 83611262823e src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Sat May 20 23:36:53 2006 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sat May 20 23:36:55 2006 +0200
@@ -772,7 +772,7 @@
 	    mk_proof (PTyDef(seg,protect_tyname name,x2p p))
 	  | x2p (xml as Elem("poracle",[],chldr)) =
 	    let
-		val (oracles,terms) = Library.partition (fn (Elem("oracle",_,_)) => true | _ => false) chldr
+		val (oracles,terms) = List.partition (fn (Elem("oracle",_,_)) => true | _ => false) chldr
 		val ors = map (fn (Elem("oracle",[("n",name)],[])) => name | xml => raise ERR "x2p" "bad oracle") oracles
 		val (c,asl) = case terms of
 				  [] => raise ERR "x2p" "Bad oracle description"
diff -r 4477003648cc -r 83611262823e 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);