# HG changeset patch
# User ballarin
# Date 1225120491 -3600
# Node ID 0dafa8aa59833750e6216a33012bb4b00e687e2b
# Parent  fc51fa5efea1c880f4dc8b839cdc38fa516075f5
Extension of interface: declarations_of.

diff -r fc51fa5efea1 -r 0dafa8aa5983 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Oct 24 17:51:36 2008 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Oct 27 16:14:51 2008 +0100
@@ -61,6 +61,9 @@
   (* Not part of the official interface.  DO NOT USE *)
   val facts_of: theory -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list list
 
+  (* Not part of the official interface.  DO NOT USE *)
+  val declarations_of: theory -> string -> declaration list * declaration list;
+
   (* Processing of locale statements *)
   val read_context_statement: xstring option -> Element.context element list ->
     (string * string list) list list -> Proof.context ->
@@ -1750,6 +1753,9 @@
 val add_term_syntax = add_decls (apsnd o cons);
 val add_declaration = add_decls (K I);
 
+fun declarations_of thy loc =
+  the_locale thy loc |> #decls |> apfst (map fst) |> apsnd (map fst);
+
 end;