src/Pure/Syntax/syn_ext.ML
changeset 29318 6337d1cb2ba0
parent 28904 3ef9489eeef5
child 29565 3f8b24fcfbd6
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Fri Jan 02 19:30:12 2009 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Fri Jan 02 19:38:13 2009 +0100
     1.3 @@ -379,7 +379,7 @@
     1.4  
     1.5  fun stamp_trfun s (c, f) = (c, (f, s));
     1.6  fun mk_trfun tr = stamp_trfun (stamp ()) tr;
     1.7 -fun eq_trfun ((_, s1:stamp), (_, s2)) = s1 = s2;
     1.8 +fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2;
     1.9  
    1.10  
    1.11  (* token translations *)
    1.12 @@ -387,7 +387,7 @@
    1.13  fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
    1.14  
    1.15  val standard_token_classes =
    1.16 -  ["class", "tfree", "tvar", "free", "bound", "var", "num", "float", "xnum", "xstr"];
    1.17 +  ["class", "tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
    1.18  
    1.19  val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
    1.20