src/Tools/induct.ML
changeset 32091 30e2ffbba718
parent 32032 a6a6e8031c14
child 32171 220abde9962b
--- a/src/Tools/induct.ML	Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Tools/induct.ML	Tue Jul 21 01:03:18 2009 +0200
@@ -124,7 +124,7 @@
 
 fun pretty_rules ctxt kind rs =
   let val thms = map snd (Item_Net.content rs)
-  in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
+  in Pretty.big_list kind (map (Display.pretty_thm ctxt) thms) end;
 
 
 (* context data *)