| changeset 11697 | 8dd899efbd35 |
| parent 6695 | d3ba5427d562 |
| child 11795 | 12a0fb3ac366 |
--- a/src/Pure/Syntax/token_trans.ML Fri Oct 05 21:42:10 2001 +0200 +++ b/src/Pure/Syntax/token_trans.ML Fri Oct 05 21:48:04 2001 +0200 @@ -51,7 +51,7 @@ fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs; val standard_token_classes = - ["class", "tfree", "tvar", "free", "bound", "var", "xnum", "xstr"]; + ["class", "tfree", "tvar", "free", "bound", "var", "num", "xnum", "xstr"];