1.1 --- a/src/Pure/ML/ml_parse.ML	Sat Aug 09 22:43:58 2008 +0200
     1.2 +++ b/src/Pure/ML/ml_parse.ML	Sat Aug 09 22:43:59 2008 +0200
     1.3 @@ -34,11 +34,12 @@
     1.4  
     1.5  (** basic parsers **)
     1.6  
     1.7 -fun $$$ x = Scan.one (fn tok => T.kind_of tok = T.Keyword andalso T.val_of tok = x) >> T.val_of;
     1.8 -val int = Scan.one (fn tok => T.kind_of tok = T.Int) >> T.val_of;
     1.9 +fun $$$ x =
    1.10 +  Scan.one (fn tok => T.kind_of tok = T.Keyword andalso T.content_of tok = x) >> T.content_of;
    1.11 +val int = Scan.one (fn tok => T.kind_of tok = T.Int) >> T.content_of;
    1.12  
    1.13 -val regular = Scan.one T.is_regular >> T.val_of;
    1.14 -val improper = Scan.one T.is_improper >> T.val_of;
    1.15 +val regular = Scan.one T.is_regular >> T.content_of;
    1.16 +val improper = Scan.one T.is_improper >> T.content_of;
    1.17  
    1.18  val blanks = Scan.repeat improper >> implode;
    1.19