src/Pure/conv.ML
changeset 23534 3f82d1798976
parent 23490 1dfbfc92017a
child 23583 00751df1f98c
     1.1 --- a/src/Pure/conv.ML	Tue Jul 03 17:17:07 2007 +0200
     1.2 +++ b/src/Pure/conv.ML	Tue Jul 03 17:17:09 2007 +0200
     1.3 @@ -33,8 +33,8 @@
     1.4    val forall_conv: int -> conv -> conv
     1.5    val concl_conv: int -> conv -> conv
     1.6    val prems_conv: int -> (int -> conv) -> conv
     1.7 -  val goals_conv: (int -> bool) -> conv -> conv
     1.8    val fconv_rule: conv -> thm -> thm
     1.9 +  val goal_conv_rule: conv -> int -> thm -> thm
    1.10  end;
    1.11  
    1.12  structure Conv: CONV =
    1.13 @@ -141,8 +141,11 @@
    1.14              | SOME (A, B) => Drule.imp_cong_rule (cv i A) (conv (i + 1) B));
    1.15    in conv 1 end;
    1.16  
    1.17 -fun goals_conv pred cv = prems_conv ~1 (fn i => if pred i then cv else all_conv);
    1.18 +fun fconv_rule cv th = Thm.equal_elim (cv (Thm.cprop_of th)) th;  (*FCONV_RULE in LCF*)
    1.19  
    1.20 -fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
    1.21 +fun goal_conv_rule cv i = Drule.with_subgoal i (fn th =>
    1.22 +  (case try (Thm.dest_implies o Thm.cprop_of) th of
    1.23 +    NONE => raise THM ("goal_conv_rule", i, [th])
    1.24 +  | SOME (A, B) => Thm.equal_elim (Drule.imp_cong_rule (cv A) (all_conv B)) th));
    1.25  
    1.26  end;