--- a/src/Pure/Isar/proof_context.ML Fri Jan 02 19:30:12 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Fri Jan 02 19:38:13 2009 +0100
@@ -408,9 +408,8 @@
("free", free_or_skolem),
("bound", plain_markup Markup.bound),
("var", var_or_skolem),
- ("num", plain_markup Markup.num),
- ("xnum", plain_markup Markup.xnum),
- ("xstr", plain_markup Markup.xstr)];
+ ("numeral", plain_markup Markup.numeral),
+ ("inner_string", plain_markup Markup.inner_string)];
in val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans)) end;