| changeset 61268 | abe08fb15a12 |
| parent 61144 | 5e94dfead1c2 |
| child 61841 | 4d3527b94f2a |
--- a/src/Tools/induct.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/Tools/induct.ML Fri Sep 25 20:37:59 2015 +0200 @@ -207,7 +207,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_item ctxt) thms) end; + in Pretty.big_list kind (map (Thm.pretty_thm_item ctxt) thms) end; (* context data *)