src/Tools/Code/code_printer.ML

--- a/src/Tools/Code/code_printer.ML	Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Tools/Code/code_printer.ML	Fri Sep 25 20:37:59 2015 +0200
@@ -111,7 +111,7 @@
 (** generic nonsense *)
 
 fun eqn_error thy (SOME thm) s =
-      error (s ^ ",\nin equation " ^ Display.string_of_thm_global thy thm)
+      error (s ^ ",\nin equation " ^ Thm.string_of_thm_global thy thm)
   | eqn_error _ NONE s = error s;
 
 val code_presentationN = "code_presentation";