# HG changeset patch
# User paulson
# Date 1073381894 -3600
# Node ID bc93ffa674cc5fcbc301cadcfdd60a03cff30b79
# Parent  ec575b7bde7a08b60b5f29f2f98d148c90bdf94a
correction to cterm_instantiate by Christoph Leuth

diff -r ec575b7bde7a -r bc93ffa674cc src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Jan 05 23:10:32 2004 +0100
+++ b/src/Pure/drule.ML	Tue Jan 06 10:38:14 2004 +0100
@@ -757,8 +757,9 @@
 in
 fun cterm_instantiate ctpairs0 th =
   let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0))
-      fun instT(ct,cu) = let val inst = subst_TVars_Vartab tye
-                         in (cterm_fun inst ct, cterm_fun inst cu) end
+      fun instT(ct,cu) = 
+        let val inst = cterm_of sign o subst_TVars_Vartab tye o term_of
+        in (inst ct, inst cu) end
       fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
   in  instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
   handle TERM _ =>