--- a/src/Pure/Syntax/syntax_phases.ML Fri Apr 08 22:59:52 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Fri Apr 08 23:09:22 2011 +0200
@@ -615,12 +615,16 @@
| token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
| token_trans _ _ = NONE;
- val markup_extern = Lexicon.unmark
- {case_class = fn x => ([Markup.tclass x], Type.extern_class (ProofContext.tsig_of ctxt) x),
- case_type = fn x => ([Markup.tycon x], Type.extern_type (ProofContext.tsig_of ctxt) x),
- case_const = fn x => ([Markup.const x], Consts.extern (ProofContext.consts_of ctxt) x),
- case_fixed = fn x => free_or_skolem ctxt x,
- case_default = fn x => ([], x)};
+ fun markup_extern c =
+ (case Syntax.lookup_const syn c of
+ SOME "" => ([], c)
+ | SOME b => markup_extern b
+ | NONE => c |> Lexicon.unmark
+ {case_class = fn x => ([Markup.tclass x], Type.extern_class (ProofContext.tsig_of ctxt) x),
+ case_type = fn x => ([Markup.tycon x], Type.extern_type (ProofContext.tsig_of ctxt) x),
+ case_const = fn x => ([Markup.const x], Consts.extern (ProofContext.consts_of ctxt) x),
+ case_fixed = fn x => free_or_skolem ctxt x,
+ case_default = fn x => ([], x)});
in
t_to_ast ctxt (Syntax.print_translation syn) t
|> Ast.normalize ctxt (Syntax.print_rules syn)