# HG changeset patch
# User haftmann
# Date 1292619654 -3600
# Node ID aad679ca38d2ac0b1b6020c31ef66fb3659ba85b
# Parent  a47133170dd0428f8cd28a7957b2bc741db30d40
more convenient order of type variables

diff -r a47133170dd0 -r aad679ca38d2 src/HOL/Tools/type_lifting.ML
--- a/src/HOL/Tools/type_lifting.ML	Fri Dec 17 21:32:06 2010 +0100
+++ b/src/HOL/Tools/type_lifting.ML	Fri Dec 17 22:00:54 2010 +0100
@@ -80,7 +80,7 @@
       let
         val names = Name.invents nctxt n k;
       in (names, fold Name.declare names nctxt) end;
-    val (((vs1, vs2), vs3), _) = Name.context
+    val (((vs3, vs2), vs1), _) = Name.context
       |> invents Name.aT (length variances)
       ||>> invents Name.aT (length variances)
       ||>> invents Name.aT (length variances);