changeset 61098 | e1b4b24f2ebd |
parent 59917 | 9830c944670f |
child 61144 | 5e94dfead1c2 |
--- a/src/Pure/simplifier.ML Wed Sep 02 23:18:39 2015 +0200 +++ b/src/Pure/simplifier.ML Wed Sep 02 23:31:41 2015 +0200 @@ -167,7 +167,7 @@ fun pretty_simproc (name, lhss) = Pretty.block (Pretty.mark_str name :: Pretty.str ":" :: Pretty.fbrk :: - Pretty.fbreaks (map (Pretty.item o single o pretty_term o Thm.term_of) lhss)); + Pretty.fbreaks (map (Pretty.item o single o pretty_term) lhss)); fun pretty_cong_name (const, name) = pretty_term ((if const then Const else Free) (name, dummyT));