# HG changeset patch
# User wenzelm
# Date 1704570007 -3600
# Node ID b5ba5b767444f6efcded1cd64fb1388233becb0e
# Parent  0875c87b4a4bf023c58ef1adc2fb5bca2686f126
minor performance tuning;

diff -r 0875c87b4a4b -r b5ba5b767444 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Sat Jan 06 15:31:41 2024 +0100
+++ b/src/Pure/zterm.ML	Sat Jan 06 20:40:07 2024 +0100
@@ -855,13 +855,13 @@
         let
           val ZTVar v = ztyp_of (unconstrain_typ T);
           val U = ztyp_of T;
-        in ZTVars.add (v, U) end));
+          val equal = (case U of ZTVar u => u = v | _ => false);
+        in not equal ? ZTVars.add (v, U) end));
     val constrain_proof =
-      map_proof_types {hyps = true} (subst_type_same (fn v =>
-        let
-          val T = ZTVar v;
-          val T' = the_default T (ZTVars.lookup constrain_instT v);
-        in if T = T' then raise Same.SAME else T' end));
+      if ZTVars.is_empty constrain_instT then I
+      else
+        map_proof_types {hyps = true}
+          (subst_type_same (Same.function (ZTVars.lookup constrain_instT)));
 
     val args = map ZClassp outer_constraints @ map (ZHyp o zterm) hyps;
     val prems = constraints @ map unconstrain_zterm hyps;