--- 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;