--- a/src/Pure/type.ML Tue Jan 09 11:57:16 2024 +0100
+++ b/src/Pure/type.ML Tue Jan 09 12:06:07 2024 +0100
@@ -334,9 +334,11 @@
(* no_tvars *)
fun no_tvars T =
- (case Term.add_tvarsT T [] of [] => T
- | vs => raise TYPE ("Illegal schematic type variable(s): " ^
- commas_quote (map (Term.string_of_vname o #1) (rev vs)), [T], []));
+ (case Term.add_tvarsT T [] of
+ [] => T
+ | vs =>
+ raise TYPE ("Illegal schematic type variable(s): " ^
+ commas_quote (map (Term.string_of_vname o #1) (rev vs)), [T], []));
(* varify_global *)