src/HOL/Tools/choice_specification.ML

                             equal_elim (symmetric rew_imp) thm
 
                         fun add_final (arg as (thy, thm)) =
                             if name = ""
                             then arg |> Library.swap
-                            else (writeln ("  " ^ name ^ ": " ^ (Display.string_of_thm thm));
+                            else (writeln ("  " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
                                   PureThy.store_thm (Binding.name name, thm) thy)
                     in
                         args |> apsnd (remove_alls frees)
                              |> apsnd undo_imps
                              |> apsnd standard