1.1 --- a/src/Pure/Isar/locale.ML	Sat Jan 17 08:30:06 2009 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Sat Jan 17 22:07:15 2009 +0100
     1.3 @@ -37,7 +37,7 @@
     1.4      thm option * thm option -> thm list ->
     1.5      (declaration * stamp) list * (declaration * stamp) list ->
     1.6      ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list ->
     1.7 -    ((string * Morphism.morphism) * stamp) list -> theory -> theory
     1.8 +    ((string * morphism) * stamp) list -> theory -> theory
     1.9  
    1.10    (* Locale name space *)
    1.11    val intern: theory -> xstring -> string
    1.12 @@ -48,9 +48,10 @@
    1.13    val params_of: theory -> string -> (Binding.T * typ option * mixfix) list
    1.14    val intros_of: theory -> string -> thm option * thm option
    1.15    val axioms_of: theory -> string -> thm list
    1.16 -  val instance_of: theory -> string -> Morphism.morphism -> term list
    1.17 +  val instance_of: theory -> string -> morphism -> term list
    1.18    val specification_of: theory -> string -> term option * term list
    1.19    val declarations_of: theory -> string -> declaration list * declaration list
    1.20 +  val dependencies_of: theory -> string -> (string * morphism) list
    1.21  
    1.22    (* Storing results *)
    1.23    val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    1.24 @@ -58,13 +59,13 @@
    1.25    val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
    1.26    val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
    1.27    val add_declaration: string -> declaration -> Proof.context -> Proof.context
    1.28 -  val add_dependency: string -> string * Morphism.morphism -> theory -> theory
    1.29 +  val add_dependency: string -> string * morphism -> theory -> theory
    1.30  
    1.31    (* Activation *)
    1.32 -  val activate_declarations: theory -> string * Morphism.morphism ->
    1.33 +  val activate_declarations: theory -> string * morphism ->
    1.34      Proof.context -> Proof.context
    1.35 -  val activate_global_facts: string * Morphism.morphism -> theory -> theory
    1.36 -  val activate_local_facts: string * Morphism.morphism -> Proof.context -> Proof.context
    1.37 +  val activate_global_facts: string * morphism -> theory -> theory
    1.38 +  val activate_local_facts: string * morphism -> Proof.context -> Proof.context
    1.39    val init: string -> theory -> Proof.context
    1.40  
    1.41    (* Reasoning about locales *)
    1.42 @@ -74,11 +75,11 @@
    1.43    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
    1.44  
    1.45    (* Registrations *)
    1.46 -  val add_registration: string * (Morphism.morphism * Morphism.morphism) ->
    1.47 +  val add_registration: string * (morphism * morphism) ->
    1.48      theory -> theory
    1.49 -  val amend_registration: Morphism.morphism -> string * Morphism.morphism ->
    1.50 +  val amend_registration: morphism -> string * morphism ->
    1.51      theory -> theory
    1.52 -  val get_registrations: theory -> (string * Morphism.morphism) list
    1.53 +  val get_registrations: theory -> (string * morphism) list
    1.54  
    1.55    (* Diagnostic *)
    1.56    val print_locales: theory -> unit
    1.57 @@ -128,7 +129,7 @@
    1.58      (* type and term syntax declarations *)
    1.59    notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
    1.60      (* theorem declarations *)
    1.61 -  dependencies: ((string * Morphism.morphism) * stamp) list
    1.62 +  dependencies: ((string * morphism) * stamp) list
    1.63      (* locale dependencies (sublocale relation) *)
    1.64  };
    1.65  
    1.66 @@ -193,6 +194,9 @@
    1.67  fun declarations_of thy name = the_locale thy name |>
    1.68    #decls |> apfst (map fst) |> apsnd (map fst);
    1.69  
    1.70 +fun dependencies_of thy name = the_locale thy name |>
    1.71 +  #dependencies |> map fst;
    1.72 +
    1.73  
    1.74  (*** Activate context elements of locale ***)
    1.75  
    1.76 @@ -389,7 +393,7 @@
    1.77  
    1.78  structure RegistrationsData = TheoryDataFun
    1.79  (
    1.80 -  type T = ((string * (Morphism.morphism * Morphism.morphism)) * stamp) list;
    1.81 +  type T = ((string * (morphism * morphism)) * stamp) list;
    1.82      (* FIXME mixins need to be stamped *)
    1.83      (* registrations, in reverse order of declaration *)
    1.84    val empty = [];