# HG changeset patch
# User wenzelm
# Date 931451464 -7200
# Node ID 4b40fb299f9f88fdb7e299c6ff5077f0290d53c2
# Parent  16ee7b14a2c14dad405c7ff3213d06b8281ba67f
improved error msgs of cterm_instantiate;
fixed incr_indexes;

diff -r 16ee7b14a2c1 -r 4b40fb299f9f src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Jul 08 18:30:21 1999 +0200
+++ b/src/Pure/drule.ML	Thu Jul 08 18:31:04 1999 +0200
@@ -386,7 +386,7 @@
   in  instantiate (map ctyp2 tye, map instT ctpairs0) th  end
   handle TERM _ =>
            raise THM("cterm_instantiate: incompatible signatures",0,[th])
-       | TYPE (msg, _, _) => raise THM("cterm_instantiate: " ^ msg, 0, [th])
+       | TYPE (msg, _, _) => raise THM(msg, 0, [th])
 end;
 
 
@@ -680,7 +680,9 @@
 
         fun inc_tvar ((x, i), S) = Some (Thm.ctyp_of sign (TVar ((x, i + inc), S)));
         fun inc_var ((x, i), T) = Some (Thm.cterm_of sign (Var ((x, i + inc), T)));
-      in instantiate' (map inc_tvar (tvars_of thm)) (map inc_var (vars_of thm)) thm end;
+        val thm' = instantiate' (map inc_tvar (tvars_of thm)) [] thm;
+        val thm'' = instantiate' [] (map inc_var (vars_of thm')) thm';
+      in thm'' end;
 
 fun incr_indexes_wrt is cTs cts thms =
   let