# 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 *)