diff -r 39acf19e9f3a -r 30e2ffbba718 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML	Tue Jul 21 01:03:18 2009 +0200
@@ -210,7 +210,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;
 
@@ -523,7 +523,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;