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