--- 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);