src/HOL/Tools/Presburger/presburger.ML

   | (Abs (s, T, t), _) => getfuncs t
   | _ => [];
 
 
 fun abstract_pres sg fm = 
-  Library.foldr (fn (t, u) =>
+  foldr (fn (t, u) =>
       let val T = fastype_of t
       in all T $ Abs ("x", T, abstract_over (t, u)) end)
-         (getfuncs fm, fm);
+         fm (getfuncs fm);
 
 
 
 (* hasfuncs_on_bounds dont care of the type of the functions applied!
  It returns true if there is a subterm coresponding to the application of

         (HOLogic.all_const T $ Abs (s, T, P), n)
       else (incr_boundvars ~1 P, n-1)
     fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
     val (rhs,irhs) = List.partition (relevant (rev ps)) hs
     val np = length ps
-    val (fm',np) =  Library.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
-      (ps,(Library.foldr HOLogic.mk_imp (rhs, c), np))
+    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
+      (foldr HOLogic.mk_imp c rhs, np) ps
     val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
       (term_frees fm' @ term_vars fm');
-    val fm2 = Library.foldr mk_all2 (vs, fm')
+    val fm2 = foldr mk_all2 fm' vs
   in (fm2, np + length vs, length rhs) end;
 
 (*Object quantifier to meta --*)
 fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;