# HG changeset patch
# User wenzelm
# Date 1138059811 -3600
# Node ID 6e97b57cdcba3a1f87fd7bd8fb1a31d23056239f
# Parent  2f064e6bea7e4ac15b6b1e5c51cabbbe34710e9f
removed the_params;

diff -r 2f064e6bea7e -r 6e97b57cdcba src/Pure/Isar/locale.ML
--- 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 *)