# HG changeset patch
# User wenzelm
# Date 1537900059 -7200
# Node ID 6ce325825ad7c2e017f0b844ab4239e46c2bf167
# Parent  5ed7206dbf184ff85a9d48de49027e91f4b4b919
tuned signature;

diff -r 5ed7206dbf18 -r 6ce325825ad7 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Sep 24 23:49:43 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Sep 25 20:27:39 2018 +0200
@@ -49,6 +49,7 @@
   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
@@ -222,7 +223,8 @@
 
 (** 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;