# HG changeset patch
# User wenzelm
# Date 1178902155 -7200
# Node ID 2afc93a3d8f4ceda707f77f233736ee388592ed0
# Parent  454f1678bf5fdfdaaf1118506c07df7f1467efe9
proper type for fun/arg_cong_rule;

diff -r 454f1678bf5f -r 2afc93a3d8f4 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri May 11 18:47:08 2007 +0200
+++ b/src/Pure/drule.ML	Fri May 11 18:49:15 2007 +0200
@@ -97,8 +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 arg_cong_rule: cterm -> thm -> thm
+  val fun_cong_rule: thm -> cterm -> thm
   val beta_eta_conversion: cterm -> thm
   val eta_long_conversion: cterm -> thm
   val eta_contraction_rule: thm -> thm