| changeset 80809 | 4a64fc4d1cde |
| parent 77846 | 5ba68d3bd741 |
| child 80952 | a61ed25ba155 |
--- a/src/Pure/Syntax/lexicon.ML Wed Sep 04 16:21:52 2024 +0200 +++ b/src/Pure/Syntax/lexicon.ML Thu Sep 05 17:39:45 2024 +0200 @@ -491,6 +491,6 @@ val _ = ML_system_pp (fn _ => fn _ => - Pretty.to_polyml o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon); + Pretty.to_ML o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon); end;