# HG changeset patch
# User wenzelm
# Date 1183586782 -7200
# Node ID 00751df1f98c407bf4a620dd10a3f834d0cd3333
# Parent  94d0dd87cc24fabbcb9e636419e34ef8dcfa5588
else_conv: only handle THM | CTERM | TERM | TYPE;
prems_conv: no index;
renamed goal_conv_rule to gconv_rule;

diff -r 94d0dd87cc24 -r 00751df1f98c src/Pure/conv.ML
--- a/src/Pure/conv.ML	Thu Jul 05 00:06:20 2007 +0200
+++ b/src/Pure/conv.ML	Thu Jul 05 00:06:22 2007 +0200
@@ -32,9 +32,9 @@
   val binop_conv: conv -> conv
   val forall_conv: int -> conv -> conv
   val concl_conv: int -> conv -> conv
-  val prems_conv: int -> (int -> conv) -> conv
+  val prems_conv: int -> conv -> conv
   val fconv_rule: conv -> thm -> thm
-  val goal_conv_rule: conv -> int -> thm -> thm
+  val gconv_rule: conv -> int -> thm -> thm
 end;
 
 structure Conv: CONV =
@@ -60,7 +60,11 @@
   end;
 
 fun (cv1 else_conv cv2) ct =
-  (case try cv1 ct of SOME eq => eq | NONE => cv2 ct);
+  (cv1 ct
+    handle THM _ => cv2 ct
+      | CTERM _ => cv2 ct
+      | TERM _ => cv2 ct
+      | TYPE _ => cv2 ct);
 
 fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv;
 fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv;
@@ -138,14 +142,14 @@
           else
             (case try Thm.dest_implies ct of
               NONE => all_conv ct
-            | SOME (A, B) => Drule.imp_cong_rule (cv i A) (conv (i + 1) B));
+            | SOME (A, B) => Drule.imp_cong_rule (cv A) (conv (i + 1) B));
   in conv 1 end;
 
 fun fconv_rule cv th = Thm.equal_elim (cv (Thm.cprop_of th)) th;  (*FCONV_RULE in LCF*)
 
-fun goal_conv_rule cv i = Drule.with_subgoal i (fn th =>
+fun gconv_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));
+    SOME (A, B) => Thm.equal_elim (Drule.imp_cong_rule (cv A) (all_conv B)) th
+  | NONE => raise THM ("gconv_rule", i, [th])));
 
 end;