src/HOL/Tools/type_lifting.ML

   let
     fun invents n k nctxt =
       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);
     fun mk_Ts vs = map2 (fn v => fn (sort, _) => TFree (v, sort))
       vs variances;