src/Pure/Isar/proof_display.ML

--- a/src/Pure/Isar/proof_display.ML	Wed Jan 10 13:33:36 2024 +0100
+++ b/src/Pure/Isar/proof_display.ML	Wed Jan 10 13:37:29 2024 +0100
@@ -94,7 +94,7 @@
       [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
 
     val tfrees = map (fn v => TFree (v, []));
-    fun pretty_type syn (t, Type.LogicalType n) =
+    fun pretty_type syn (t, Type.Logical_Type n) =
           if syn then NONE
           else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n))))
       | pretty_type syn (t, Type.Abbreviation (vs, U, syn')) =