# HG changeset patch
# User wenzelm
# Date 1537819525 -7200
# Node ID 5eda37c06f4226257166260b64d39a4caa5eb082
# Parent  da448868a18a2f51d966c661170b4b2c7486fe7b
tuned signature;

diff -r da448868a18a -r 5eda37c06f42 src/Pure/Isar/locale.ML
--- 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;
 
diff -r da448868a18a -r 5eda37c06f42 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Mon Sep 24 20:24:03 2018 +0200
+++ b/src/Pure/morphism.ML	Mon Sep 24 22:05:25 2018 +0200
@@ -24,6 +24,7 @@
     fact: (thm list -> thm list) list} -> morphism
   val pretty: morphism -> Pretty.T
   val binding: morphism -> binding -> binding
+  val binding_prefix: morphism -> (string * bool) list
   val typ: morphism -> typ -> typ
   val term: morphism -> term -> term
   val fact: morphism -> thm list -> thm list
@@ -88,6 +89,7 @@
 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
 
 fun binding (Morphism {binding, ...}) = apply binding;
+fun binding_prefix morph = Binding.name "x" |> binding morph |> Binding.prefix_of;
 fun typ (Morphism {typ, ...}) = apply typ;
 fun term (Morphism {term, ...}) = apply term;
 fun fact (Morphism {fact, ...}) = apply fact;