# HG changeset patch # User wenzelm # Date 1162759472 -3600 # Node ID 99f546731724c72b928c7a7dcd929dd5097aa738 # Parent c3618fc6a6f752bdfa87c3d713822376b479fe6d Sign.const_syntax_name; diff -r c3618fc6a6f7 -r 99f546731724 src/HOL/HOL.thy --- 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