src/Pure/ML/ml_pretty.ML
changeset 80857 aff85c86737b
parent 80856 300c75231e2b
child 81121 7cacedbddba7
--- a/src/Pure/ML/ml_pretty.ML	Wed Sep 11 19:53:35 2024 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Wed Sep 11 19:59:10 2024 +0200
@@ -38,8 +38,8 @@
     SOME (ContextProperty (_, b)) => b
   | _ => "");
 
-val markup_bg = "begin";
-val markup_en = "end";
+val markup_bg = "markup_bg";
+val markup_en = "markup_en";
 
 fun context_markup context =
   let