src/Pure/Isar/proof_context.ML

     | (used, _) => used));
 
 val ins_occs = foldl_term_types (fn t => foldl_atyps
   (fn (tab, TFree (x, _)) => Symtab.update_multi ((x, t), tab) | (tab, _) => tab));
 
-fun ins_skolem def_ty = Library.foldr
+fun ins_skolem def_ty = foldr
   (fn ((x, x'), types) =>
     (case def_ty x' of
       SOME T => Vartab.update (((x, ~1), T), types)
     | NONE => types));
 

 
 fun declare_occ (ctxt as Context {asms = (_, fixes), ...}, t) =
   declare_syn (ctxt, t)
   |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs (occ, t)))
   |> map_defaults (fn (types, sorts, used, occ) =>
-      (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) (fixes, types), sorts, used, occ));
+      (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) types fixes, sorts, used, occ));
 
 in
 
 fun declare_term t ctxt = declare_occ (ctxt, t);
 fun declare_terms ts ctxt = Library.foldl declare_occ (ctxt, ts);

       then gen else a :: gen;
   in fn tfrees => Library.foldl add ([], tfrees) end;
 
 fun generalize inner outer ts =
   let
-    val tfrees = generalize_tfrees inner outer (Library.foldr Term.add_term_tfree_names (ts, []));
+    val tfrees = generalize_tfrees inner outer (foldr Term.add_term_tfree_names [] ts);
     fun gen (x, S) = if x mem_string tfrees then TVar ((x, 0), S) else TFree (x, S);
   in map (Term.map_term_types (Term.map_type_tfree gen)) ts end;
 
 
 

   let
     fun replace (opt_x :: xs) ((y, T) :: ys) = (getOpt (opt_x,y), T) :: replace xs ys
       | replace [] ys = ys
       | replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt);
   in
-    if null (Library.foldr Term.add_typ_tvars (map snd fixes, [])) andalso
-      null (Library.foldr Term.add_term_vars (List.concat (map snd assumes), [])) then
+    if null (foldr Term.add_typ_tvars [] (map snd fixes)) andalso
+      null (foldr Term.add_term_vars [] (List.concat (map snd assumes))) then
         {fixes = replace xs fixes, assumes = assumes, binds = map drop_schematic binds}
     else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt)
   end;
 
 fun get_case (ctxt as Context {cases, ...}) name xs =