src/Pure/Isar/locale.ML

   val params_of: theory -> string -> ((string * typ) * mixfix) list
   val intros_of: theory -> string -> thm option * thm option
   val axioms_of: theory -> string -> thm list
   val instance_of: theory -> string -> morphism -> term list
   val specification_of: theory -> string -> term option * term list
+  val hyp_spec_of: theory -> string -> Element.context_i list
 
   (* Storing results *)
   val add_facts: string -> string -> Attrib.fact list -> Proof.context -> Proof.context
   val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
 

   val activate_fragment: registration -> local_theory -> local_theory
   val registrations_of: Context.generic -> string -> (string * morphism) list
   val add_dependency: string -> registration -> theory -> theory
 
   (* Diagnostic *)
-  val hyp_spec_of: theory -> string -> Element.context_i list
   val print_locales: bool -> theory -> unit
   val print_locale: theory -> bool -> xstring * Position.T -> unit
   val print_registrations: Proof.context -> xstring * Position.T -> unit
   val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
   val pretty_locale: theory -> bool -> string -> Pretty.T list

 fun instance_of thy name morph = params_of thy name |>
   map (Morphism.term morph o Free o #1);
 
 fun specification_of thy = #spec o the_locale thy;
 
-fun dependencies_of thy name = the_locale thy name |>
-  #dependencies;
+fun hyp_spec_of thy = #hyp_spec o the_locale thy;
+
+fun dependencies_of thy = #dependencies o the_locale thy;
 
 fun mixins_of thy name serial = the_locale thy name |>
   #mixins |> lookup_mixins serial;
 
 (* FIXME unused!? *)

     "back-chain all introduction rules of locales");
 
 
 (*** diagnostic commands and interfaces ***)
 
-fun hyp_spec_of thy = #hyp_spec o the_locale thy;
-
 fun print_locales verbose thy =
   Pretty.block
     (Pretty.breaks
       (Pretty.str "locales:" ::
         map (Pretty.mark_str o #1)