# HG changeset patch
# User wenzelm
# Date 927656490 -7200
# Node ID ac968ce542a87735739c265df8e254df86ae491d
# Parent  b91772e592dc83bfbb95451d4a0a195025ab42d5
renamed Comment.empty to Comment.none;

diff -r b91772e592dc -r ac968ce542a8 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Tue May 25 20:21:05 1999 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Tue May 25 20:21:30 1999 +0200
@@ -156,7 +156,7 @@
 (* formal comments *)
 
 val comment = text >> Comment.plain;
-val marg_comment = Scan.optional ($$$ "--" |-- comment) Comment.empty;
+val marg_comment = Scan.optional ($$$ "--" |-- comment) Comment.none;
 val interest = Scan.optional ($$$ "%" >> K Comment.no_interest) Comment.default_interest;