| changeset 62819 | d3ff367a16a0 |
| parent 62663 | bea354f6ff21 |
| child 67650 | 5e4f9a0ffea5 |
--- a/src/Pure/morphism.ML Sat Apr 02 20:33:34 2016 +0200 +++ b/src/Pure/morphism.ML Sat Apr 02 21:10:07 2016 +0200 @@ -71,7 +71,7 @@ fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names)); -val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty); +val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty); fun binding (Morphism {binding, ...}) = apply binding; fun typ (Morphism {typ, ...}) = apply typ;