# HG changeset patch
# User wenzelm
# Date 1183475829 -7200
# Node ID 3f82d17989762ddbf81c14bfead32e4020635412
# Parent  b86b764d576437c94389f5886bccb914e7ce3cd1
removed obsolete goals_conv (cf. prems_conv);
added efficient goal_conv_rule;
tuned comments;

diff -r b86b764d5764 -r 3f82d1798976 src/Pure/conv.ML
--- a/src/Pure/conv.ML	Tue Jul 03 17:17:07 2007 +0200
+++ b/src/Pure/conv.ML	Tue Jul 03 17:17:09 2007 +0200
@@ -33,8 +33,8 @@
   val forall_conv: int -> conv -> conv
   val concl_conv: int -> conv -> conv
   val prems_conv: int -> (int -> conv) -> conv
-  val goals_conv: (int -> bool) -> conv -> conv
   val fconv_rule: conv -> thm -> thm
+  val goal_conv_rule: conv -> int -> thm -> thm
 end;
 
 structure Conv: CONV =
@@ -141,8 +141,11 @@
             | SOME (A, B) => Drule.imp_cong_rule (cv i A) (conv (i + 1) B));
   in conv 1 end;
 
-fun goals_conv pred cv = prems_conv ~1 (fn i => if pred i then cv else all_conv);
+fun fconv_rule cv th = Thm.equal_elim (cv (Thm.cprop_of th)) th;  (*FCONV_RULE in LCF*)
 
-fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
+fun goal_conv_rule cv i = Drule.with_subgoal i (fn th =>
+  (case try (Thm.dest_implies o Thm.cprop_of) th of
+    NONE => raise THM ("goal_conv_rule", i, [th])
+  | SOME (A, B) => Thm.equal_elim (Drule.imp_cong_rule (cv A) (all_conv B)) th));
 
 end;