# HG changeset patch
# User paulson
# Date 1175506268 -7200
# Node ID 705d4fb9e628250adb080b008095b015987e3310
# Parent  f19ddf96c323601f73f40cc01ac56935c8aabe7c
optimizing the null instantiation case

diff -r f19ddf96c323 -r 705d4fb9e628 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Apr 02 11:30:44 2007 +0200
+++ b/src/Pure/drule.ML	Mon Apr 02 11:31:08 2007 +0200
@@ -893,7 +893,8 @@
           handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
     in  (thy', tye', maxi')  end;
 in
-fun cterm_instantiate ctpairs0 th =
+fun cterm_instantiate [] th = th
+  | cterm_instantiate ctpairs0 th =
   let val (thy,tye,_) = foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0
       fun instT(ct,cu) =
         let val inst = cterm_of thy o Term.map_types (Envir.norm_type tye) o term_of