# HG changeset patch
# User wenzelm
# Date 1183475831 -7200
# Node ID ecf487dce798637f9d3e9163db7962600c13a69f
# Parent  60a1672e298e37fa9526e0a6e8cf33229e425c50
tuned rotate_prems;
tuned comments;

diff -r 60a1672e298e -r ecf487dce798 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Jul 03 17:17:11 2007 +0200
+++ b/src/Pure/drule.ML	Tue Jul 03 17:17:11 2007 +0200
@@ -443,7 +443,9 @@
  end;
 
 (*Rotates a rule's premises to the left by k*)
-val rotate_prems = permute_prems 0;
+fun rotate_prems 0 = I
+  | rotate_prems k = permute_prems 0 k;
+
 fun with_subgoal i f = rotate_prems (i - 1) #> f #> rotate_prems (1 - i);
 
 (* permute prems, where the i-th position in the argument list (counting from 0)
@@ -585,8 +587,8 @@
 
 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*)
+fun arg_cong_rule ct th = Thm.combination (Thm.reflexive ct) th;    (*AP_TERM in LCF/HOL*)
+fun fun_cong_rule th ct = Thm.combination th (Thm.reflexive ct);    (*AP_THM in LCF/HOL*)
 
 local
   val dest_eq = Thm.dest_equals o cprop_of