fixed INST: has same semantic now as INST_TYPE for repetitions

--- a/src/HOL/Import/proof_kernel.ML	Mon Sep 12 23:27:12 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Tue Sep 13 17:05:59 2005 +0200
@@ -1329,7 +1329,7 @@
 	val _ = if_debug (app (fn (x,y) => (prin x; prin y))) sigma
 	val _ = if_debug pth hth
 	val sg = sign_of thy
-	val (sdom,srng) = ListPair.unzip sigma
+	val (sdom,srng) = ListPair.unzip (rev sigma)
 	val th = hthm2thm hth
 	val th1 = mk_INST (map (cterm_of sg) sdom) (map (cterm_of sg) srng) th
 	val res = HOLThm([],th1)