src/HOL/Tools/old_inductive_package.ML

                HOLogic.mk_Trueprop (valOf (pred_of u) $ t)))
       end;
 
     val ind_prems = map mk_ind_prem intr_ts;
 
-    val factors = Library.fold (mg_prod_factors preds) ind_prems [];
+    val factors = fold (mg_prod_factors preds) ind_prems [];
 
     (* make conclusions for induction rules *)
 
     fun mk_ind_concl ((c, P), (ts, x)) =
       let val T = HOLogic.dest_setT (fastype_of c);

 
 
 (* external interfaces *)
 
 fun try_term f msg thy t =
-  (case Library.try f t of
+  (case try f t of
     SOME x => x
   | NONE => error (msg ^ Sign.string_of_term thy t));
 
 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs pre_intros monos thy =
   let