# HG changeset patch
# User wenzelm
# Date 1137951959 -3600
# Node ID b38a18c9aed9492d5d9172d03f10bc8bd9e89f0c
# Parent  ada43d36eaf794251f19053cc98d5cfe9bd6b769
added the_params;

diff -r ada43d36eaf7 -r b38a18c9aed9 src/Pure/Isar/locale.ML
--- 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 *)