--- a/src/Pure/Isar/outer_parse.ML Wed Dec 22 20:28:56 1999 +0100
+++ b/src/Pure/Isar/outer_parse.ML Wed Dec 22 20:29:19 1999 +0100
@@ -161,8 +161,8 @@
(* formal comments *)
-val comment = text >> Comment.plain;
-val marg_comment = Scan.optional ($$$ "--" |-- comment) Comment.none;
+val comment = text >> (Comment.plain o Library.single);
+val marg_comment = Scan.repeat ($$$ "--" |-- text) >> Comment.plain;
val interest = Scan.optional ($$$ "%%" >> K Comment.no_interest ||
$$$ "%" |-- Scan.optional nat 1 >> Comment.interest) Comment.default_interest;