--- 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;