# HG changeset patch
# User clasohm
# Date 830858581 -7200
# Node ID e22ad43bab5f74b430d03ec3584c68df8295a604
# Parent  4aa538e82f7681424c277aa401cb641a770eb66c
moved dest_cimplies to drule.ML; added adjust_maxidx

diff -r 4aa538e82f76 -r e22ad43bab5f src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Apr 30 11:08:09 1996 +0200
+++ b/src/Pure/drule.ML	Tue Apr 30 12:03:01 1996 +0200
@@ -35,6 +35,7 @@
   val forall_elim_vars	: int -> thm -> thm
   val implies_elim_list	: thm -> thm list -> thm
   val implies_intr_list	: cterm list -> thm -> thm
+  val dest_cimplies     : cterm -> cterm * cterm
   val MRL		: thm list list * thm list -> thm list
   val MRS		: thm list * thm -> thm
   val read_instantiate	: (string*string)list -> thm -> thm
@@ -192,6 +193,17 @@
 
 (** some cterm->cterm operations: much faster than calling cterm_of! **)
 
+(*dest_implies for cterms. Note T=prop below*)
+fun dest_cimplies ct =
+  (let val (ct1, ct2) = dest_comb ct
+       val {t, ...} = rep_cterm ct1;
+   in case head_of t of
+          Const("==>", _) => (snd (dest_comb ct1), ct2)
+        | _ => raise TERM ("dest_cimplies", [term_of ct])
+   end
+  ) handle CTERM "dest_comb" => raise TERM ("dest_cimplies", [term_of ct]);
+
+
 (*Discard flexflex pairs; return a cterm*)
 fun cskip_flexpairs ct =
     case term_of ct of
@@ -511,7 +523,7 @@
 (*Do not rewrite flex-flex pairs*)
 fun goals_conv pred cv =
   let fun gconv i ct =
-        let val (A,B) = Thm.dest_cimplies ct
+        let val (A,B) = dest_cimplies ct
             val (thA,j) = case term_of A of
                   Const("=?=",_)$_$_ => (reflexive A, i)
                 | _ => (if pred i then cv A else reflexive A, i+1)
diff -r 4aa538e82f76 -r e22ad43bab5f src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Apr 30 11:08:09 1996 +0200
+++ b/src/Pure/thm.ML	Tue Apr 30 12:03:01 1996 +0200
@@ -26,9 +26,9 @@
   val read_cterm        : Sign.sg -> string * typ -> cterm
   val read_cterms       : Sign.sg -> string list * typ list -> cterm list
   val cterm_fun         : (term -> term) -> (cterm -> cterm)
-  val dest_cimplies     : cterm -> cterm * cterm
   val dest_comb         : cterm -> cterm * cterm
   val dest_abs          : cterm -> cterm * cterm
+  val adjust_maxidx     : cterm -> cterm
   val capply            : cterm -> cterm -> cterm
   val cabs              : cterm -> cterm -> cterm
   val read_def_cterm    :
@@ -195,12 +195,6 @@
 fun cterm_fun f (Cterm {sign, t, ...}) = cterm_of sign (f t);
 
 
-(*dest_implies for cterms. Note T=prop below*)
-fun dest_cimplies (Cterm{sign, T, maxidx, t=Const("==>", _) $ A $ B}) =
-       (Cterm{sign=sign, T=T, maxidx=maxidx, t=A},
-        Cterm{sign=sign, T=T, maxidx=maxidx, t=B})
-  | dest_cimplies ct = raise TERM ("dest_cimplies", [term_of ct]);
-
 exception CTERM of string;
 
 (*Destruct application in cterms*)
@@ -223,6 +217,9 @@
       end
   | dest_abs _ = raise CTERM "dest_abs";
 
+fun adjust_maxidx (Cterm {sign, T, t, ...}) =
+  Cterm {sign = sign, T = T, maxidx = maxidx_of_term t, t = t}
+
 (*Form cterm out of a function and an argument*)
 fun capply (Cterm {t=f, sign=sign1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
            (Cterm {t=x, sign=sign2, T, maxidx=maxidx2}) =