# HG changeset patch
# User wenzelm
# Date 1704380163 -3600
# Node ID 17e06494a4da374b3c31cdc46f00b41dd5e17503
# Parent  4c3346b4b10084e4d8ac714da1553ad50f2a04d4
tuned;

diff -r 4c3346b4b100 -r 17e06494a4da src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Thu Jan 04 15:49:09 2024 +0100
+++ b/src/Pure/zterm.ML	Thu Jan 04 15:56:03 2024 +0100
@@ -556,7 +556,8 @@
 fun ztyp_of (TFree (a, S)) = ZTVar ((a, ~1), S)
   | ztyp_of (TVar v) = ZTVar v
   | ztyp_of (Type ("fun", [T, U])) = ZFun (ztyp_of T, ztyp_of U)
-  | ztyp_of (Type (c, [])) = if c = "prop" then ZProp else ZType0 c
+  | ztyp_of (Type ("prop", [])) = ZProp
+  | ztyp_of (Type (c, [])) = ZType0 c
   | ztyp_of (Type (c, [T])) = ZType1 (c, ztyp_of T)
   | ztyp_of (Type (c, ts)) = ZType (c, map ztyp_of ts);