# HG changeset patch
# User haftmann
# Date 1501827157 -7200
# Node ID 489667636064afcc48021cf45cb15b775c188c48
# Parent  f773691617c0be725cbf6ec8a07647affcca4841
compactified output

diff -r f773691617c0 -r 489667636064 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Aug 03 12:50:03 2017 +0200
+++ b/src/Pure/Isar/code.ML	Fri Aug 04 08:12:37 2017 +0200
@@ -1072,7 +1072,7 @@
       end;
 
 fun pretty_cert _ (Nothing _) =
-      [Pretty.str "(unimplemented)"]
+      []
   | pretty_cert thy (cert as Equations _) =
       (map_filter
         (Option.map (Thm.pretty_thm_global thy o
diff -r f773691617c0 -r 489667636064 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Thu Aug 03 12:50:03 2017 +0200
+++ b/src/Tools/Code/code_preproc.ML	Fri Aug 04 08:12:37 2017 +0200
@@ -306,7 +306,9 @@
     AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
     |> (map o apfst) (Code.string_of_const thy)
     |> sort (string_ord o apply2 fst)
-    |> map (fn (s, cert) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: Code.pretty_cert thy cert))
+    |> (map o apsnd) (Code.pretty_cert thy)
+    |> filter_out (null o snd)
+    |> map (fn (s, ps) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: ps))
     |> Pretty.chunks
   end;