| changeset 51580 | 64ef8260dc60 |
| parent 49748 | a346daa8a1f4 |
| child 51584 | 98029ceda8ce |
--- a/src/Tools/induct.ML Fri Mar 29 22:13:02 2013 +0100 +++ b/src/Tools/induct.ML Fri Mar 29 22:14:27 2013 +0100 @@ -213,7 +213,7 @@ fun pretty_rules ctxt kind rs = let val thms = map snd (Item_Net.content rs) - in Pretty.big_list kind (map (Display.pretty_thm ctxt) thms) end; + in Pretty.big_list kind (map (Pretty.item o single o Display.pretty_thm ctxt) thms) end; (* context data *)