src/Pure/thm.ML

   val term_of           : cterm -> term
   val cterm_of          : Sign.sg -> term -> cterm
   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    :
     Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
     string list -> bool -> string * typ -> cterm * (indexname * typ) list

   end;
 
 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*)
 fun dest_comb (Cterm{sign, T, maxidx, t = A $ B}) =
       let val typeA = fastype_of A;

       let val (y,N) = variant_abs (x,ty,M)
       in (Cterm {sign = sign, T = ty, maxidx = 0, t = Free(y,ty)},
           Cterm {sign = sign, T = S, maxidx = maxidx, t = N})
       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}) =
       if T = dty then Cterm{t=f$x, sign=Sign.merge(sign1,sign2), T=rty,