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)