# HG changeset patch
# User berghofe
# Date 1091115921 -7200
# Node ID 666f89fbb860cf7e50ee4a000983ab6d17a17da2
# Parent  e6a2a98d5ef5470ea26c95fe61b08b9aed2d39ad
- optimized nodup_vars check in capply
- new function dest_ctyp

diff -r e6a2a98d5ef5 -r 666f89fbb860 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Jul 29 16:57:41 2004 +0200
+++ b/src/Pure/thm.ML	Thu Jul 29 17:45:21 2004 +0200
@@ -110,6 +110,7 @@
 signature THM =
 sig
   include BASIC_THM
+  val dest_ctyp         : ctyp -> ctyp list
   val dest_comb         : cterm -> cterm * cterm
   val dest_abs          : string option -> cterm -> cterm * cterm
   val capply            : cterm -> cterm -> cterm
@@ -153,6 +154,10 @@
 fun read_ctyp sign s =
   Ctyp {sign_ref = Sign.self_ref sign, T = Sign.read_typ (sign, K None) s};
 
+fun dest_ctyp (Ctyp {sign_ref, T = Type (s, Ts)}) =
+      map (fn T => Ctyp {sign_ref = sign_ref, T = T}) Ts
+  | dest_ctyp ct = [ct];
+
 
 
 (** certified terms **)
@@ -214,7 +219,9 @@
 fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
            (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) =
       if T = dty then
-        Cterm{t=Sign.nodup_vars (f$x), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty,
+        Cterm{t = if maxidx1 >= 0 andalso maxidx2 >= 0 then Sign.nodup_vars (f $ x)
+            else f $ x,  (*no new Vars: no expensive check!*)
+          sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty,
           maxidx=Int.max(maxidx1, maxidx2)}
       else raise CTERM "capply: types don't agree"
   | capply _ _ = raise CTERM "capply: first arg is not a function"