| changeset 11503 | 4c25eef6f325 |
| parent 10150 | a068c666c53e |
| child 14174 | f3cafd2929d5 |
--- a/src/Pure/Isar/args.ML Thu Aug 16 23:19:12 2001 +0200 +++ b/src/Pure/Isar/args.ML Tue Aug 21 20:09:09 2001 +0200 @@ -222,7 +222,7 @@ fun dest_src (Src src) = src; fun err_in_src kind msg (Src ((s, args), pos)) = - error (kind ^ " " ^ s ^ Position.str_of pos ^ ": " ^ msg ^ "\n " ^ + error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": " ^ msg ^ "\n " ^ space_implode " " (map str_of args));