src/Provers/simp.ML

 	      Abs(_,_,body) => add_term_vars(body,hvars)
 	    | _$_ => let val (f,args) = strip_comb tm 
 		     in case f of
 			    Const(c,T) => 
 				if c mem ccs
-				then Library.foldr add_hvars (args,hvars)
+				then foldr add_hvars hvars args
 				else add_term_vars(tm,hvars)
 			  | _ => add_term_vars(tm,hvars)
 		     end
 	    | _ => hvars;
   in add_hvars end;

 fun add_new_asm_vars new_asms =
     let fun itf((tm,at),vars) =
 		if at then vars else add_term_vars(tm,vars)
 	fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
 		in if length(tml)=length(al)
-		   then Library.foldr itf (tml~~al,vars)
+		   then foldr itf vars (tml~~al)
 		   else vars
 		end
 	fun add_vars (tm,vars) = case tm of
 		  Abs (_,_,body) => add_vars(body,vars)
 		| r$s => (case head_of tm of

 (* thm': [?z -> l; Prems; r -> ?t] ==> ?z -> ?t *)
     val nops = nprems_of thm'
     val lhs = rhs_of_eq 1 thm'
     val rhs = lhs_of_eq nops thm'
     val asms = tl(rev(tl(prems_of thm')))
-    val hvars = Library.foldr (add_hidden_vars ccs) (lhs::rhs::asms,[])
+    val hvars = foldr (add_hidden_vars ccs) [] (lhs::rhs::asms)
     val hvars = add_new_asm_vars new_asms (rhs,hvars)
     fun it_asms (asm,hvars) =
 	if atomic asm then add_new_asm_vars new_asms (asm,hvars)
 	else add_term_frees(asm,hvars)
-    val hvars = Library.foldr it_asms (asms,hvars)
+    val hvars = foldr it_asms hvars asms
     val hvs = map (#1 o dest_Var) hvars
     val refl1_tac = refl_tac 1
     fun norm_step_tac st = st |>
 	 (case head_of(rhs_of_eq 1 st) of
 	    Var(ixn,_) => if ixn mem hvs then refl1_tac

   Net.insert_term((concl_of th, th), net, Drule.eq_thm_prop)
   handle Net.INSERT => 
     (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
      net);
 
-val insert_thms = Library.foldr insert_thm_warn;
+val insert_thms = foldr insert_thm_warn;
 
 fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
               splits,split_consts}, thm) =
 let val thms = mk_simps thm
 in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps,
-      simps = (thm,thms)::simps, simp_net = insert_thms(thms,simp_net),
+      simps = (thm,thms)::simps, simp_net = insert_thms simp_net thms,
       splits=splits,split_consts=split_consts}
 end;
 
 val op addrews = Library.foldl addrew;
 
 fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
                    splits,split_consts}, thms) =
 let val congs' = thms @ congs;
 in SS{auto_tac=auto_tac, congs= congs',
-      cong_net= insert_thms (map mk_trans thms,cong_net),
+      cong_net= insert_thms cong_net (map mk_trans thms),
       mk_simps= normed_rews congs', simps=simps, simp_net=simp_net,
       splits=splits,split_consts=split_consts}
 end;
 
 fun split_err() = error("split rule not of the form ?P(c(...)) = ...");

   Net.delete_term((concl_of th, th), net, Drule.eq_thm_prop)
   handle Net.DELETE => 
     (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
      net);
 
-val delete_thms = Library.foldr delete_thm_warn;
+val delete_thms = foldr delete_thm_warn;
 
 fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
                    splits,split_consts}, thms) =
 let val congs' = Library.foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
 in SS{auto_tac=auto_tac, congs= congs',
-      cong_net= delete_thms(map mk_trans thms,cong_net),
+      cong_net= delete_thms cong_net (map mk_trans thms),
       mk_simps= normed_rews congs', simps=simps, simp_net=simp_net,
       splits=splits,split_consts=split_consts}
 end;
 
 fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,

       | find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
 			   print_thm thm;
 			   ([],simps'))
     val (thms,simps') = find(simps,[])
 in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
-      simps = simps', simp_net = delete_thms(thms,simp_net),
+      simps = simps', simp_net = delete_thms simp_net thms,
       splits=splits,split_consts=split_consts}
 end;
 
 val op delrews = Library.foldl delrew;
 

 fun add_asms(ss,thm,a,anet,ats,cs) =
     let val As = strip_varify(nth_subgoal i thm, a, []);
 	val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
 	val new_rws = flat(map mk_rew_rules thms);
 	val rwrls = map mk_trans (flat(map mk_rew_rules thms));
-	val anet' = Library.foldr lhs_insert_thm (rwrls,anet)
+	val anet' = foldr lhs_insert_thm anet rwrls
     in  if !tracing andalso not(null new_rws)
 	then (writeln"Adding rewrites:";  prths new_rws;  ())
 	else ();
 	(ss,thm,anet',anet::ats,cs) 
     end;