| changeset 80809 | 4a64fc4d1cde |
| parent 78759 | 461e924cc825 |
--- a/src/Pure/morphism.ML Wed Sep 04 16:21:52 2024 +0200 +++ b/src/Pure/morphism.ML Thu Sep 05 17:39:45 2024 +0200 @@ -140,7 +140,7 @@ fun pretty phi = Pretty.enum ";" "{" "}" (map Pretty.str (rev (#names (rep phi)))); -val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty); +val _ = ML_system_pp (fn _ => fn _ => Pretty.to_ML o pretty); val binding = apply #binding; fun binding_prefix morph = Binding.name "x" |> binding morph |> Binding.prefix_of;