# HG changeset patch
# User wenzelm
# Date 1704570067 -3600
# Node ID 6f852d23306a560a62b1180a90b35dc18d771d19
# Parent  b5ba5b767444f6efcded1cd64fb1388233becb0e
tuned;

diff -r b5ba5b767444 -r 6f852d23306a src/Pure/zterm.ML
--- 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 =