# HG changeset patch
# User wenzelm
# Date 1519416728 -3600
# Node ID a0b58be402abaa98b008daf98e202262a897feab
# Parent  041898537c1961a17e1a713d2c9eeec657b4468c
tuned signature;

diff -r 041898537c19 -r a0b58be402ab src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Feb 23 20:55:46 2018 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Feb 23 21:12:08 2018 +0100
@@ -166,9 +166,10 @@
 
 (* Instantiation morphism *)
 
-fun inst_morphism (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
+fun inst_morphism params ((prfx, mandatory), insts') ctxt =
   let
     (* parameters *)
+    val parm_types = map #2 params;
     val type_parms = fold Term.add_tfreesT parm_types [];
 
     (* type inference *)
@@ -189,7 +190,7 @@
       (type_parms ~~ map Logic.dest_type type_parms'')
       |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T));
     val cert_inst =
-      ((parm_names ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'')
+      ((map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'')
       |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t));
   in
     (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $>
@@ -315,7 +316,7 @@
 fun finish_inst ctxt (loc, (prfx, inst)) =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val (morph, _) = inst_morphism (Locale.params_types_of thy loc) (prfx, inst) ctxt;
+    val (morph, _) = inst_morphism (map #1 (Locale.params_of thy loc)) (prfx, inst) ctxt;
   in (loc, morph) end;
 
 fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) =>
@@ -376,19 +377,18 @@
 
     fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) =
       let
-        val (parm_names, parm_types) = Locale.params_types_of thy loc;
-        val inst' = prep_inst ctxt parm_names inst;
+        val params = map #1 (Locale.params_of thy loc);
+        val inst' = prep_inst ctxt (map #1 params) inst;
         val eqns' = map (apsnd (parse_eqn ctxt)) eqns;
-        val parm_types' = parm_types
-          |> map (Logic.varifyT_global #>
+        val parm_types' =
+          params |> map (#2 #> Logic.varifyT_global #>
               Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #>
               Type_Infer.paramify_vars);
         val inst'' = map2 Type.constraint parm_types' inst';
         val insts' = insts @ [(loc, (prfx, inst''))];
         val eqnss' = eqnss @ [eqns'];
         val ((insts'', eqnss'', _, _), _) = check_autofix insts' eqnss' [] [] ctxt;
-        val (inst_morph, _) =
-          inst_morphism (parm_names, parm_types) (prfx, #2 (#2 (List.last insts''))) ctxt;
+        val (inst_morph, _) = inst_morphism params (prfx, #2 (#2 (List.last insts''))) ctxt;
         val rewrite_morph =
           List.last eqnss''
           |> map (snd #> Thm.cterm_of ctxt #> Thm.assume #> Local_Defs.abs_def_rule ctxt)
diff -r 041898537c19 -r a0b58be402ab src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Feb 23 20:55:46 2018 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Feb 23 21:12:08 2018 +0100
@@ -49,7 +49,6 @@
   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
@@ -213,7 +212,6 @@
 (** 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;