--- 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"
--- 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);