--- a/src/HOL/HOL.thy Sun Nov 05 09:36:25 2006 +0100
+++ b/src/HOL/HOL.thy Sun Nov 05 21:44:32 2006 +0100
@@ -208,12 +208,11 @@
typed_print_translation {*
let
+ val syntax_name = Sign.const_syntax_name (the_context ());
fun tr' c = (c, fn show_sorts => fn T => fn ts =>
if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
-in
- map (tr' o prefix Syntax.constN) ["HOL.one", "HOL.zero"]
-end;
+in map (tr' o Sign.const_syntax_name (the_context ())) ["HOL.one", "HOL.zero"] end;
*} -- {* show types that are presumably too general *}
const_syntax