Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
no_variables: tuned error msg;
authorwenzelm
Sat, 20 Oct 2007 18:54:30 +0200
changeset 25117 74b279146ecb
parent 25116 31551aae280f
child 25118 158149a6e95b
no_variables: tuned error msg;
src/Pure/sign.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle