src/Pure/Isar/outer_parse.ML
changeset 12876 a70df1e5bf10
parent 12272 9bc50336dab6
child 12942 48fbe245879e
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Tue Feb 12 20:25:58 2002 +0100
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Tue Feb 12 20:28:27 2002 +0100
     1.3 @@ -45,9 +45,6 @@
     1.4    val xname: token list -> xstring * token list
     1.5    val text: token list -> string * token list
     1.6    val uname: token list -> string option * token list
     1.7 -  val comment: token list -> Comment.text * token list
     1.8 -  val marg_comment: token list -> Comment.text * token list
     1.9 -  val interest: token list -> Comment.interest * token list
    1.10    val sort: token list -> string * token list
    1.11    val arity: token list -> (string list * string) * token list
    1.12    val simple_arity: token list -> (string list * xclass) * token list
    1.13 @@ -177,15 +174,6 @@
    1.14  val uname = underscore >> K None || name >> Some;
    1.15  
    1.16  
    1.17 -(* formal comments *)
    1.18 -
    1.19 -val comment = text >> (Comment.plain o Library.single);
    1.20 -val marg_comment = Scan.repeat ($$$ "--" |-- text) >> Comment.plain;
    1.21 -
    1.22 -val interest = Scan.optional ($$$ "%%" >> K Comment.no_interest ||
    1.23 -  $$$ "%" |-- Scan.optional nat 1 >> Comment.interest) Comment.default_interest;
    1.24 -
    1.25 -
    1.26  (* sorts and arities *)
    1.27  
    1.28  val sort = group "sort" xname;