src/Pure/Isar/code.ML

         (tyscm, SOME [((abstractions o dest_eqn o Thm.prop_of) concrete_thm,
           (SOME (Thm.varifyT_global abs_thm), true))])
       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
             Axclass.overload (Proof_Context.init_global thy)) o fst o snd)
          o these o snd o equations_of_cert thy) cert