src/HOL/HOL.thy

 translations
   (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
 
 typed_print_translation {*
 let
-  val syntax_name = Sign.const_syntax_name (the_context ());
+  val thy = 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 Sign.const_syntax_name (the_context ())) ["HOL.one", "HOL.zero"] end;
+in map (tr' o Sign.const_syntax_name thy) ["HOL.one", "HOL.zero"] end;
 *} -- {* show types that are presumably too general *}
 
 notation
   uminus  ("- _" [81] 80)