--- 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}) =