# HG changeset patch # User haftmann # Date 1496690679 -7200 # Node ID cc8e9289a6c403307a8a5c09367804d5e7138c1f # Parent 08ab52fb9db5c428a6274dfa3304fe06f84a37e7 clarified message diff -r 08ab52fb9db5 -r cc8e9289a6c4 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Tue Jun 06 13:42:38 2017 +0200 +++ b/src/Pure/Isar/code.ML Mon Jun 05 21:24:39 2017 +0200 @@ -883,7 +883,7 @@ end; fun pretty_cert thy (cert as Nothing _) = - [Pretty.str "(not implemented)"] + [Pretty.str "(no equations)"] | pretty_cert thy (cert as Equations _) = (map_filter (Option.map (Thm.pretty_thm_global thy o