diff -r 08cf9aaf3aa1 -r 454f1678bf5f src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri May 11 18:46:50 2007 +0200
+++ b/src/Pure/drule.ML	Fri May 11 18:47:08 2007 +0200
@@ -97,6 +97,8 @@
   val del_rule: thm -> thm list -> thm list
   val merge_rules: thm list * thm list -> thm list
   val imp_cong_rule: thm -> thm -> thm
+  val fun_cong_rule: cterm -> thm -> thm
+  val arg_cong_rule: thm -> cterm -> thm
   val beta_eta_conversion: cterm -> thm
   val eta_long_conversion: cterm -> thm
   val eta_contraction_rule: thm -> thm
@@ -579,7 +581,10 @@
         (implies_elim (implies_elim (assume BAC) (assume B)) (assume A))))))
   end;
 
-val imp_cong_rule = combination o combination (reflexive implies);
+val imp_cong_rule = Thm.combination o Thm.combination (Thm.reflexive implies);
+
+fun arg_cong_rule ct th = Thm.combination (Thm.reflexive ct) th;    (*AP_TERM*)
+fun fun_cong_rule th ct = Thm.combination th (Thm.reflexive ct);    (*AP_THM*)
 
 local
   val dest_eq = Thm.dest_equals o cprop_of