--- a/src/Pure/drule.ML Wed Jan 03 11:14:48 2001 +0100
+++ b/src/Pure/drule.ML Wed Jan 03 21:18:31 2001 +0100
@@ -123,15 +123,15 @@
fun dest_implies ct =
case term_of ct of
(Const("==>", _) $ _ $ _) =>
- let val (ct1,ct2) = dest_comb ct
- in (#2 (dest_comb ct1), ct2) end
+ let val (ct1,ct2) = Thm.dest_comb ct
+ in (#2 (Thm.dest_comb ct1), ct2) end
| _ => raise TERM ("dest_implies", [term_of ct]) ;
fun dest_equals ct =
case term_of ct of
(Const("==", _) $ _ $ _) =>
- let val (ct1,ct2) = dest_comb ct
- in (#2 (dest_comb ct1), ct2) end
+ let val (ct1,ct2) = Thm.dest_comb ct
+ in (#2 (Thm.dest_comb ct1), ct2) end
| _ => raise TERM ("dest_equals", [term_of ct]) ;
@@ -151,7 +151,7 @@
(* A1==>...An==>B goes to B, where B is not an implication *)
fun strip_imp_concl ct =
case term_of ct of (Const("==>", _) $ _ $ _) =>
- strip_imp_concl (#2 (dest_comb ct))
+ strip_imp_concl (#2 (Thm.dest_comb ct))
| _ => ct;
(*The premises of a theorem, as a cterm list*)
@@ -162,7 +162,7 @@
val implies = cterm_of proto_sign Term.implies;
(*cterm version of mk_implies*)
-fun mk_implies(A,B) = capply (capply implies A) B;
+fun mk_implies(A,B) = Thm.capply (Thm.capply implies A) B;
(*cterm version of list_implies: [A1,...,An], B goes to [|A1;==>;An|]==>B *)
fun list_implies([], B) = B
--- a/src/Pure/meta_simplifier.ML Wed Jan 03 11:14:48 2001 +0100
+++ b/src/Pure/meta_simplifier.ML Wed Jan 03 21:18:31 2001 +0100
@@ -696,7 +696,7 @@
(case term_of t0 of
Abs (a, T, t) =>
let val b = variant bounds a
- val (v, t') = dest_abs (Some ("." ^ b)) t0
+ val (v, t') = Thm.dest_abs (Some ("." ^ b)) t0
val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless)
val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0
in case botc skel' mss' t' of
@@ -719,7 +719,7 @@
val (tskel, uskel) = case skel of
tskel $ uskel => (tskel, uskel)
| _ => (skel0, skel0);
- val (ct, cu) = dest_comb t0
+ val (ct, cu) = Thm.dest_comb t0
in
(case botc tskel mss ct of
Some thm1 =>
@@ -742,7 +742,7 @@
(let
val thm = congc (prover mss, sign, maxidx) cong t0;
val t = rhs_of thm;
- val (cl, cr) = dest_comb t
+ val (cl, cr) = Thm.dest_comb t
val dVar = Var(("", 0), dummyT)
val skel =
list_comb (h, replicate (length ts) dVar)
--- a/src/Pure/tctical.ML Wed Jan 03 11:14:48 2001 +0100
+++ b/src/Pure/tctical.ML Wed Jan 03 21:18:31 2001 +0100
@@ -374,7 +374,7 @@
val prop_equals = cterm_of (Theory.sign_of ProtoPure.thy)
(Const("==", propT-->propT-->propT));
-fun mk_prop_equals(t,u) = capply (capply prop_equals t) u;
+fun mk_prop_equals(t,u) = Thm.capply (Thm.capply prop_equals t) u;
(*Like trivial but returns [ct==X] ct==>X instead of ct==>ct, if possible.
It is paired with a function to undo the transformation. If ct contains
--- a/src/Pure/thm.ML Wed Jan 03 11:14:48 2001 +0100
+++ b/src/Pure/thm.ML Wed Jan 03 21:18:31 2001 +0100
@@ -27,11 +27,7 @@
val ctyp_of_term : cterm -> ctyp
val read_cterm : Sign.sg -> string * typ -> cterm
val cterm_fun : (term -> term) -> (cterm -> cterm)
- val dest_comb : cterm -> cterm * cterm
- val dest_abs : string option -> 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
@@ -153,6 +149,10 @@
signature THM =
sig
include BASIC_THM
+ val dest_comb : cterm -> cterm * cterm
+ val dest_abs : string option -> cterm -> cterm * cterm
+ val capply : cterm -> cterm -> cterm
+ val cabs : cterm -> cterm -> cterm
val major_prem_of : thm -> term
val no_prems : thm -> bool
val no_attributes : 'a -> 'a * 'b attribute list