# 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