src/Pure/Isar/locale.ML
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;