src/Pure/Isar/local_defs.ML
changeset 32091 30e2ffbba718
parent 31794 71af1fd6a5e4
child 33385 fb2358edcfb6
     1.1 --- a/src/Pure/Isar/local_defs.ML	Tue Jul 21 00:56:19 2009 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Tue Jul 21 01:03:18 2009 +0200
     1.3 @@ -196,7 +196,7 @@
     1.4  
     1.5  fun print_rules ctxt =
     1.6    Pretty.writeln (Pretty.big_list "definitional transformations:"
     1.7 -    (map (ProofContext.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
     1.8 +    (map (Display.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
     1.9  
    1.10  val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
    1.11  val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);