src/Pure/simplifier.ML
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));