--- a/src/Pure/Isar/outer_parse.ML Tue Feb 12 20:25:58 2002 +0100
+++ b/src/Pure/Isar/outer_parse.ML Tue Feb 12 20:28:27 2002 +0100
@@ -45,9 +45,6 @@
val xname: token list -> xstring * token list
val text: token list -> string * token list
val uname: token list -> string option * token list
- val comment: token list -> Comment.text * token list
- val marg_comment: token list -> Comment.text * token list
- val interest: token list -> Comment.interest * token list
val sort: token list -> string * token list
val arity: token list -> (string list * string) * token list
val simple_arity: token list -> (string list * xclass) * token list
@@ -177,15 +174,6 @@
val uname = underscore >> K None || name >> Some;
-(* formal comments *)
-
-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;
-
-
(* sorts and arities *)
val sort = group "sort" xname;