| changeset 17335 | 7cff05c90a0e |
| parent 17328 | 7bbfb79eda96 |
| child 17379 | 85109eec887b |
--- 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)