| changeset 62663 | bea354f6ff21 |
| parent 62505 | 9e2a65912111 |
| child 62819 | d3ff367a16a0 |
--- a/src/Pure/morphism.ML Thu Mar 17 16:56:44 2016 +0100 +++ b/src/Pure/morphism.ML Fri Mar 18 16:26:35 2016 +0100 @@ -71,6 +71,8 @@ fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names)); +val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty); + fun binding (Morphism {binding, ...}) = apply binding; fun typ (Morphism {typ, ...}) = apply typ; fun term (Morphism {term, ...}) = apply term;