src/HOL/Tools/specification_package.ML
changeset 26928 ca87aff1ad2d
parent 26481 92e901171cc8
child 26939 1035c89b4c02
--- a/src/HOL/Tools/specification_package.ML	Fri May 16 23:25:37 2008 +0200
+++ b/src/HOL/Tools/specification_package.ML	Sat May 17 13:54:30 2008 +0200
@@ -184,7 +184,7 @@
                         fun add_final (arg as (thy, thm)) =
                             if name = ""
                             then arg |> Library.swap
-                            else (writeln ("  " ^ name ^ ": " ^ (string_of_thm thm));
+                            else (writeln ("  " ^ name ^ ": " ^ (Display.string_of_thm thm));
                                   PureThy.store_thm (name, thm) thy)
                     in
                         args |> apsnd (remove_alls frees)