src/Pure/Isar/locale.ML

   val check: theory -> xstring * Position.T -> string
   val extern: theory -> string -> xstring
   val markup_name: Proof.context -> string -> string
   val pretty_name: Proof.context -> string -> Pretty.T
   val defined: theory -> string -> bool
+  val parameters_of: theory -> string -> (string * sort) list * ((string * typ) * mixfix) list
   val params_of: theory -> string -> ((string * typ) * mixfix) 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
   val specification_of: theory -> string -> term option * term list

 
 
 
 (** Primitive operations **)
 
-fun params_of thy = snd o #parameters o the_locale thy;
+fun parameters_of thy = #parameters o the_locale thy;
+val params_of = #2 oo parameters_of;
 
 fun intros_of thy = (apply2 o Option.map) (Thm.transfer thy) o #intros o the_locale thy;
 
 fun axioms_of thy = map (Thm.transfer thy) o #axioms o the_locale thy;