diff -r 0b6217fda81b -r abe08fb15a12 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Fri Sep 25 20:37:59 2015 +0200
@@ -78,7 +78,7 @@
      Pretty.chunks (map (fn (b, th) => Pretty.block
        [Binding.pretty b, Pretty.str ":",
         Pretty.brk 1,
-        Display.pretty_thm ctxt th])
+        Thm.pretty_thm ctxt th])
           defs),
 
      Pretty.str "Verification conditions:",