diff -r d5060a919b3f -r 86b9a405b0cc src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Mar 20 18:33:56 2023 +0100
+++ b/src/Tools/Code/code_thingol.ML	Fri Mar 24 18:30:17 2023 +0000
@@ -15,28 +15,28 @@
 
 signature BASIC_CODE_THINGOL =
 sig
-  type vname = string;
+  type vname = string
   datatype dict =
       Dict of (class * class) list * plain_dict
   and plain_dict = 
       Dict_Const of (string * class) * dict list list
-    | Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool };
+    | Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool }
   datatype itype =
       `%% of string * itype list
-    | ITyVar of vname;
+    | ITyVar of vname
   type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
-    dom: itype list, range: itype, annotation: itype option };
+    dom: itype list, range: itype, annotation: itype option }
   datatype iterm =
       IConst of const
     | IVar of vname option
     | `$ of iterm * iterm
     | `|=> of (vname option * itype) * (iterm * itype)
-    | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
-  val `-> : itype * itype -> itype;
-  val `--> : itype list * itype -> itype;
-  val `$$ : iterm * iterm list -> iterm;
-  val `|==> : (vname option * itype) list * (iterm * itype) -> iterm;
-  type typscheme = (vname * sort) list * itype;
+    | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm }
+  val `-> : itype * itype -> itype
+  val `--> : itype list * itype -> itype
+  val `$$ : iterm * iterm list -> iterm
+  val `|==> : (vname option * itype) list * (iterm * itype) -> iterm
+  type typscheme = (vname * sort) list * itype
 end;
 
 signature CODE_THINGOL =