--- a/src/Pure/Isar/local_defs.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/Pure/Isar/local_defs.ML Sat Mar 30 13:40:19 2013 +0100
@@ -181,7 +181,7 @@
fun print_rules ctxt =
Pretty.writeln (Pretty.big_list "definitional transformations:"
- (map (Display.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
+ (map (Display.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);