--- a/src/Pure/Isar/locale.ML Sun Jan 22 18:45:58 2006 +0100
+++ b/src/Pure/Isar/locale.ML Sun Jan 22 18:45:59 2006 +0100
@@ -41,6 +41,7 @@
val intern: theory -> xstring -> string
val extern: theory -> string -> xstring
+ val the_params: theory -> string -> (string * typ) list
val init: string -> theory -> Proof.context
(* Processing of locale statements *) (* FIXME export more abstract version *)
@@ -318,6 +319,10 @@
SOME loc => loc
| NONE => error ("Unknown locale " ^ quote name));
+fun the_params thy name =
+ let val {params = (ps, _), ...} = the_locale thy name
+ in map fst ps end;
+
(* access registrations *)