changeset 69062 | 5eda37c06f42 |
parent 69061 | da448868a18a |
child 69063 | 765ff343a7aa |
--- a/src/Pure/Isar/locale.ML Mon Sep 24 20:24:03 2018 +0200 +++ b/src/Pure/Isar/locale.ML Mon Sep 24 22:05:25 2018 +0200 @@ -259,7 +259,7 @@ let val thy = Proof_Context.theory_of ctxt; val morph' = morph $> export; - val qs = Binding.name "x" |> Morphism.binding morph' |> Binding.prefix_of; + val qs = Morphism.binding_prefix morph'; val ts = instance_of thy name morph'; in pretty_reg_inst ctxt qs (name, ts) end;