diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Fri Sep 25 20:37:59 2015 +0200
@@ -148,7 +148,7 @@
             fun add_final (thm, thy) =
               if name = ""
               then (thm, thy)
-              else (writeln ("  " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
+              else (writeln ("  " ^ name ^ ": " ^ Thm.string_of_thm_global thy thm);
                 Global_Theory.store_thm (Binding.name name, thm) thy)
           in
             swap args