# HG changeset patch
# User wenzelm
# Date 1192899270 -7200
# Node ID 74b279146ecbf3d6fd1fb444b024170ee38f898d
# Parent  31551aae280f0c4693c33d8de10973585064febf
no_variables: tuned error msg;

diff -r 31551aae280f -r 74b279146ecb src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Oct 20 18:54:29 2007 +0200
+++ b/src/Pure/sign.ML	Sat Oct 20 18:54:30 2007 +0200
@@ -442,9 +442,9 @@
 fun no_variables kind add addT mk mkT pp tm =
   (case (add tm [], addT tm []) of
     ([], []) => tm
-  | (frees, tfrees) => error (Pretty.string_of (Pretty.block (Pretty.breaks
-      (Pretty.str ("Illegal " ^ kind ^ " variable(s) in term:") ::
-       map (Pretty.term pp o mk) frees @ map (Pretty.typ pp o mkT) tfrees)))));
+  | (frees, tfrees) => error (Pretty.string_of (Pretty.block
+      (Pretty.str ("Illegal " ^ kind ^ " variable(s) in term:") :: Pretty.brk 1 ::
+       Pretty.commas (map (Pretty.term pp o mk) frees @ map (Pretty.typ pp o mkT) tfrees)))));
 
 val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree;
 val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar;