# HG changeset patch
# User wenzelm
# Date 1519164208 -3600
# Node ID ab68ca1e80ba84963eebae4217b5cdafc99ca878
# Parent  00c43648839802ef0899ecd019427a0e6d7ac719
tuned signature;

diff -r 00c436488398 -r ab68ca1e80ba src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/Pure/Isar/expression.ML	Tue Feb 20 23:03:28 2018 +0100
@@ -309,8 +309,7 @@
 fun finish_inst ctxt (loc, (prfx, inst)) =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
-    val (morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst) ctxt;
+    val (morph, _) = inst_morphism (Locale.params_types_of thy loc) (prfx, inst) ctxt;
   in (loc, morph) end;
 
 fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) =>
@@ -371,7 +370,7 @@
 
     fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) =
       let
-        val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
+        val (parm_names, parm_types) = Locale.params_types_of thy loc;
         val inst' = prep_inst ctxt parm_names inst;
         val eqns' = map (apsnd (parse_eqn ctxt)) eqns;
         val parm_types' = parm_types
diff -r 00c436488398 -r ab68ca1e80ba src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Feb 20 23:03:28 2018 +0100
@@ -49,6 +49,7 @@
   val pretty_name: Proof.context -> string -> Pretty.T
   val defined: theory -> string -> bool
   val params_of: theory -> string -> ((string * typ) * mixfix) list
+  val params_types_of: theory -> string -> string list * typ list
   val intros_of: theory -> string -> thm option * thm option
   val axioms_of: theory -> string -> thm list
   val instance_of: theory -> string -> morphism -> term list
@@ -212,6 +213,7 @@
 (** Primitive operations **)
 
 fun params_of thy = snd o #parameters o the_locale thy;
+fun params_types_of thy loc = split_list (map #1 (params_of thy loc));
 
 fun intros_of thy = (apply2 o Option.map) (Thm.transfer thy) o #intros o the_locale thy;