# HG changeset patch
# User wenzelm
# Date 1218314639 -7200
# Node ID 78cae5cca09ebb25a3a4d421084bbea003d91be8
# Parent  0dfed2f2822abcdf7885d1d509c06d7aab6bd2f9
renamed ML_Lex.val_of to content_of;

diff -r 0dfed2f2822a -r 78cae5cca09e src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sat Aug 09 22:43:58 2008 +0200
+++ b/src/Pure/ML/ml_lex.ML	Sat Aug 09 22:43:59 2008 +0200
@@ -16,7 +16,7 @@
   val is_improper: token -> bool
   val pos_of: token -> string
   val kind_of: token -> token_kind
-  val val_of: token -> string
+  val content_of: token -> string
   val keywords: string list
   val source: (Symbol.symbol, 'a) Source.source ->
     (token, (SymbolPos.T, Position.T * (Symbol.symbol, 'a) Source.source)
@@ -59,8 +59,8 @@
 
 (* token content *)
 
-fun val_of (Token (_, (_, x))) = x;
-fun token_leq (tok, tok') = val_of tok <= val_of tok';
+fun content_of (Token (_, (_, x))) = x;
+fun token_leq (tok, tok') = content_of tok <= content_of tok';
 
 fun kind_of (Token (_, (k, _))) = k;
 
diff -r 0dfed2f2822a -r 78cae5cca09e src/Pure/ML/ml_parse.ML
--- a/src/Pure/ML/ml_parse.ML	Sat Aug 09 22:43:58 2008 +0200
+++ b/src/Pure/ML/ml_parse.ML	Sat Aug 09 22:43:59 2008 +0200
@@ -34,11 +34,12 @@
 
 (** basic parsers **)
 
-fun $$$ x = Scan.one (fn tok => T.kind_of tok = T.Keyword andalso T.val_of tok = x) >> T.val_of;
-val int = Scan.one (fn tok => T.kind_of tok = T.Int) >> T.val_of;
+fun $$$ x =
+  Scan.one (fn tok => T.kind_of tok = T.Keyword andalso T.content_of tok = x) >> T.content_of;
+val int = Scan.one (fn tok => T.kind_of tok = T.Int) >> T.content_of;
 
-val regular = Scan.one T.is_regular >> T.val_of;
-val improper = Scan.one T.is_improper >> T.val_of;
+val regular = Scan.one T.is_regular >> T.content_of;
+val improper = Scan.one T.is_improper >> T.content_of;
 
 val blanks = Scan.repeat improper >> implode;