# HG changeset patch
# User obua
# Date 1126623959 -7200
# Node ID 7cff05c90a0e27171768cedbd6d6985bdb5ce506
# Parent  6e5815f4d770372ae71c0724ddc50da94216c981
fixed INST: has same semantic now as INST_TYPE for repetitions

diff -r 6e5815f4d770 -r 7cff05c90a0e src/HOL/Import/proof_kernel.ML
--- 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)