src/Tools/Code/code_preproc.ML
changeset 66332 489667636064
parent 65026 49c537d87896
child 69593 3dda49e08b9d
--- 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;