src/Pure/Isar/expression.ML

 (** Finish locale elements **)
 
 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) =>
   let val x = Binding.name_of binding
   in (binding, AList.lookup (op =) parms x, mx) end);

 
     val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
 
     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
           |> map (Type_Infer.paramify_vars o
               Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global);