src/Pure/Isar/locale.ML
changeset 28691 0dafa8aa5983
parent 28375 c879d88d038a
child 28710 e2064974c114
     1.1 --- a/src/Pure/Isar/locale.ML	Fri Oct 24 17:51:36 2008 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon Oct 27 16:14:51 2008 +0100
     1.3 @@ -61,6 +61,9 @@
     1.4    (* Not part of the official interface.  DO NOT USE *)
     1.5    val facts_of: theory -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list list
     1.6  
     1.7 +  (* Not part of the official interface.  DO NOT USE *)
     1.8 +  val declarations_of: theory -> string -> declaration list * declaration list;
     1.9 +
    1.10    (* Processing of locale statements *)
    1.11    val read_context_statement: xstring option -> Element.context element list ->
    1.12      (string * string list) list list -> Proof.context ->
    1.13 @@ -1750,6 +1753,9 @@
    1.14  val add_term_syntax = add_decls (apsnd o cons);
    1.15  val add_declaration = add_decls (K I);
    1.16  
    1.17 +fun declarations_of thy loc =
    1.18 +  the_locale thy loc |> #decls |> apfst (map fst) |> apsnd (map fst);
    1.19 +
    1.20  end;
    1.21  
    1.22