tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;

--- a/src/Pure/drule.ML	Sat Nov 05 20:07:38 2011 +0100
+++ b/src/Pure/drule.ML	Sat Nov 05 20:32:12 2011 +0100
@@ -816,7 +816,7 @@
 
 
 
-(*** Instantiate theorem th, reading instantiations in theory thy ****)
+(** variations on Thm.instantiate **)
 
 fun instantiate_normalize instpair th =
   Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl);
@@ -843,23 +843,20 @@
 in
 
 fun cterm_instantiate [] th = th
-  | cterm_instantiate ctpairs0 th =
+  | cterm_instantiate ctpairs th =
       let
-        val (thy, tye, _) = fold_rev add_types ctpairs0 (Thm.theory_of_thm th, Vartab.empty, 0);
+        val (thy, tye, _) = fold_rev add_types ctpairs (Thm.theory_of_thm th, Vartab.empty, 0);
         val certT = ctyp_of thy;
-        fun instT (ct, cu) =
-          let val inst = cterm_of thy o Term.map_types (Envir.norm_type tye) o term_of
-          in (inst ct, inst cu) end;
-        fun ctyp2 (ixn, (S, T)) = (certT (TVar (ixn, S)), certT (Envir.norm_type tye T));
-      in instantiate_normalize (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th end
-      handle TERM _ => raise THM ("cterm_instantiate: incompatible theories", 0, [th])
+        val instT =
+          Vartab.fold (fn (xi, (S, T)) =>
+            cons (certT (TVar (xi, S)), certT (Envir.norm_type tye T))) tye [];
+        val inst = map (pairself (Thm.instantiate_cterm (instT, []))) ctpairs;
+      in instantiate_normalize (instT, inst) th end
+      handle TERM (msg, _) => raise THM (msg, 0, [th])
         | TYPE (msg, _, _) => raise THM (msg, 0, [th]);
 end;
 
 
-
-(** variations on instantiate **)
-
 (* instantiate by left-to-right occurrence of variables *)
 
 fun instantiate' cTs cts thm =