diff -r 2a0645733185 -r 7913823f14e3 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Wed Jul 22 10:49:26 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML	Wed Jul 22 11:23:09 2009 +0200
@@ -214,7 +214,7 @@
   |> 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;
 
@@ -529,7 +529,7 @@
       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;