src/Pure/drule.ML
changeset 23537 ecf487dce798
parent 23439 8c7da8649f2f
child 23568 afecdba16452
--- 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