src/Tools/Code/code_preproc.ML

   |> (map o apfst) (Code.string_of_const thy)
   |> sort (string_ord o pairself fst)
   |> map (fn (s, thms) =>
        (Pretty.block o Pretty.fbreaks) (
          Pretty.str s
-         :: map (Display.pretty_thm o fst) thms
+         :: map (Display.pretty_thm_global thy o fst) thms
        ))
   |> Pretty.chunks;
 
 
 (** the Waisenhaus algorithm **)

       let
         val thm3 = postprocess_conv thy (Thm.rhs_of thm2);
       in
         Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
           error ("could not construct evaluation proof:\n"
-          ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
+          ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
       end;
   in gen_eval thy I conclude_evaluation end;
 
 fun eval thy postproc evaluator = gen_eval thy (Thm.cterm_of thy)
   (K o postproc (postprocess_term thy)) (simple_evaluator evaluator);