diff -r f5bce5af361b -r 725438ceae7c src/Pure/ML/ml_pp.ML
--- a/src/Pure/ML/ml_pp.ML	Mon Jul 22 21:55:02 2019 +0200
+++ b/src/Pure/ML/ml_pp.ML	Tue Jul 23 12:07:50 2019 +0200
@@ -80,7 +80,6 @@
     | PAxm a => prt_app "PAxm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
     | OfClass a => prt_app "OfClass" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
     | Oracle a => prt_app "Oracle" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
-    | Promise a => prt_app "Promise" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
     | PThm a => prt_app "PThm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))))
 
 and prt_proofs parens dp prf =