| changeset 62819 | d3ff367a16a0 |
| parent 62782 | 057e8dbe4326 |
| child 64275 | ac2abc987cf9 |
--- a/src/Pure/Syntax/lexicon.ML Sat Apr 02 20:33:34 2016 +0200 +++ b/src/Pure/Syntax/lexicon.ML Sat Apr 02 21:10:07 2016 +0200 @@ -451,7 +451,7 @@ (* toplevel pretty printing *) val _ = - PolyML.addPrettyPrinter (fn _ => fn _ => + ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon); end;