# HG changeset patch
# User wenzelm
# Date 978553111 -3600
# Node ID 8fa4aafa73143937380509af10744fbc5af124b9
# Parent  ace2ba2d4fd16deee846b653a1e8219fc2fd5fb9
Thm: dest_comb, dest_abs, capply, cabs no longer global;

diff -r ace2ba2d4fd1 -r 8fa4aafa7314 src/Pure/drule.ML
--- 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
diff -r ace2ba2d4fd1 -r 8fa4aafa7314 src/Pure/meta_simplifier.ML
--- 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)
diff -r ace2ba2d4fd1 -r 8fa4aafa7314 src/Pure/tctical.ML
--- 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
diff -r ace2ba2d4fd1 -r 8fa4aafa7314 src/Pure/thm.ML
--- 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