diff -r 909dcdec2122 -r dea94b1aabc3 src/Pure/ML_Bootstrap.thy --- a/src/Pure/ML_Bootstrap.thy Wed Dec 06 15:46:35 2017 +0100 +++ b/src/Pure/ML_Bootstrap.thy Wed Dec 06 18:59:33 2017 +0100 @@ -34,7 +34,7 @@ \ \ -ML \@{assert} (not (can ML \open RunCall\))\ +ML \\<^assert> (not (can ML \open RunCall\))\ subsection \Switch to bootstrap environment\