diff -r 0b6217fda81b -r abe08fb15a12 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Isar/context_rules.ML	Fri Sep 25 20:37:59 2015 +0200
@@ -121,7 +121,7 @@
     fun prt_kind (i, b) =
       Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
         (map_filter (fn (_, (k, th)) =>
-            if k = (i, b) then SOME (Display.pretty_thm_item ctxt th) else NONE)
+            if k = (i, b) then SOME (Thm.pretty_thm_item ctxt th) else NONE)
           (sort (int_ord o apply2 fst) rules));
   in Pretty.writeln_chunks (map prt_kind rule_kinds) end;