tuned;

--- a/src/Pure/zterm.ML	Sat Jan 06 20:40:07 2024 +0100
+++ b/src/Pure/zterm.ML	Sat Jan 06 20:41:07 2024 +0100
@@ -853,8 +853,7 @@
     val constrain_instT =
       ZTVars.build (present_set |> Types.fold (fn (T, _) =>
         let
-          val ZTVar v = ztyp_of (unconstrain_typ T);
-          val U = ztyp_of T;
+          val ZTVar v = ztyp_of (unconstrain_typ T) and U = ztyp_of T;
           val equal = (case U of ZTVar u => u = v | _ => false);
         in not equal ? ZTVars.add (v, U) end));
     val constrain_proof =