--- a/src/HOL/Library/EfficientNat.thy Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Library/EfficientNat.thy Fri Mar 04 15:07:34 2005 +0100
@@ -191,8 +191,8 @@
let val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
in
if forall (can (dest o concl_of)) ths andalso
- exists (fn th => "Suc" mem Library.foldr add_term_consts
- (List.mapPartial (try dest) (concl_of th :: prems_of th), [])) ths
+ exists (fn th => "Suc" mem foldr add_term_consts
+ [] (List.mapPartial (try dest) (concl_of th :: prems_of th))) ths
then remove_suc_clause thy ths else ths
end;