# HG changeset patch
# User wenzelm
# Date 1704798367 -3600
# Node ID a5f327d9466f7baabf79faa52948c18789bdb317
# Parent  57d29f537723541807d3c6db3d7ff53a6a9f7b97
tuned whitespace;

diff -r 57d29f537723 -r a5f327d9466f src/Pure/type.ML
--- 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 *)