src/Pure/conv.ML
changeset 23583 00751df1f98c
parent 23534 3f82d1798976
child 23587 46d01f5e1e5b
     1.1 --- a/src/Pure/conv.ML	Thu Jul 05 00:06:20 2007 +0200
     1.2 +++ b/src/Pure/conv.ML	Thu Jul 05 00:06:22 2007 +0200
     1.3 @@ -32,9 +32,9 @@
     1.4    val binop_conv: conv -> conv
     1.5    val forall_conv: int -> conv -> conv
     1.6    val concl_conv: int -> conv -> conv
     1.7 -  val prems_conv: int -> (int -> conv) -> conv
     1.8 +  val prems_conv: int -> conv -> conv
     1.9    val fconv_rule: conv -> thm -> thm
    1.10 -  val goal_conv_rule: conv -> int -> thm -> thm
    1.11 +  val gconv_rule: conv -> int -> thm -> thm
    1.12  end;
    1.13  
    1.14  structure Conv: CONV =
    1.15 @@ -60,7 +60,11 @@
    1.16    end;
    1.17  
    1.18  fun (cv1 else_conv cv2) ct =
    1.19 -  (case try cv1 ct of SOME eq => eq | NONE => cv2 ct);
    1.20 +  (cv1 ct
    1.21 +    handle THM _ => cv2 ct
    1.22 +      | CTERM _ => cv2 ct
    1.23 +      | TERM _ => cv2 ct
    1.24 +      | TYPE _ => cv2 ct);
    1.25  
    1.26  fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv;
    1.27  fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv;
    1.28 @@ -138,14 +142,14 @@
    1.29            else
    1.30              (case try Thm.dest_implies ct of
    1.31                NONE => all_conv ct
    1.32 -            | SOME (A, B) => Drule.imp_cong_rule (cv i A) (conv (i + 1) B));
    1.33 +            | SOME (A, B) => Drule.imp_cong_rule (cv A) (conv (i + 1) B));
    1.34    in conv 1 end;
    1.35  
    1.36  fun fconv_rule cv th = Thm.equal_elim (cv (Thm.cprop_of th)) th;  (*FCONV_RULE in LCF*)
    1.37  
    1.38 -fun goal_conv_rule cv i = Drule.with_subgoal i (fn th =>
    1.39 +fun gconv_rule cv i = Drule.with_subgoal i (fn th =>
    1.40    (case try (Thm.dest_implies o Thm.cprop_of) th of
    1.41 -    NONE => raise THM ("goal_conv_rule", i, [th])
    1.42 -  | SOME (A, B) => Thm.equal_elim (Drule.imp_cong_rule (cv A) (all_conv B)) th));
    1.43 +    SOME (A, B) => Thm.equal_elim (Drule.imp_cong_rule (cv A) (all_conv B)) th
    1.44 +  | NONE => raise THM ("gconv_rule", i, [th])));
    1.45  
    1.46  end;