--- a/src/Pure/Isar/local_defs.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/Isar/local_defs.ML Tue Jul 21 01:03:18 2009 +0200
@@ -196,7 +196,7 @@
fun print_rules ctxt =
Pretty.writeln (Pretty.big_list "definitional transformations:"
- (map (ProofContext.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
+ (map (Display.pretty_thm 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);