src/Pure/Isar/proof_context.ML
changeset 29318 6337d1cb2ba0
parent 29006 abe0f11cfa4e
child 29581 b3b33e0298eb
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Jan 02 19:30:12 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Jan 02 19:38:13 2009 +0100
     1.3 @@ -408,9 +408,8 @@
     1.4     ("free", free_or_skolem),
     1.5     ("bound", plain_markup Markup.bound),
     1.6     ("var", var_or_skolem),
     1.7 -   ("num", plain_markup Markup.num),
     1.8 -   ("xnum", plain_markup Markup.xnum),
     1.9 -   ("xstr", plain_markup Markup.xstr)];
    1.10 +   ("numeral", plain_markup Markup.numeral),
    1.11 +   ("inner_string", plain_markup Markup.inner_string)];
    1.12  
    1.13  in val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans)) end;
    1.14