--- a/src/Pure/Isar/locale.ML Tue Jan 24 00:43:29 2006 +0100
+++ b/src/Pure/Isar/locale.ML Tue Jan 24 00:43:31 2006 +0100
@@ -41,7 +41,6 @@
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 *)
@@ -319,10 +318,6 @@
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 *)