1.1 --- a/src/Pure/Isar/locale.ML	Sat Mar 28 12:26:21 2009 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Sat Mar 28 12:48:31 2009 +0100
     1.3 @@ -109,8 +109,10 @@
     1.4  fun mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies)) =
     1.5    Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
     1.6      decls = decls, notes = notes, dependencies = dependencies};
     1.7 +
     1.8  fun map_locale f (Loc {parameters, spec, intros, axioms, decls, notes, dependencies}) =
     1.9    mk_locale (f ((parameters, spec, intros, axioms), ((decls, notes), dependencies)));
    1.10 +
    1.11  fun merge_locale (Loc {parameters, spec, intros, axioms, decls = (decls1, decls2),
    1.12    notes, dependencies}, Loc {decls = (decls1', decls2'), notes = notes',
    1.13      dependencies = dependencies', ...}) = mk_locale
    1.14 @@ -178,20 +180,16 @@
    1.15  
    1.16  (** Identifiers: activated locales in theory or proof context **)
    1.17  
    1.18 -type identifiers = (string * term list) list;
    1.19 -
    1.20 -val empty = ([] : identifiers);
    1.21 -
    1.22  fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
    1.23  
    1.24  local
    1.25  
    1.26 -datatype 'a delayed = Ready of 'a | ToDo of ('a delayed * 'a delayed);
    1.27 +datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
    1.28  
    1.29  structure Identifiers = GenericDataFun
    1.30  (
    1.31 -  type T = identifiers delayed;
    1.32 -  val empty = Ready empty;
    1.33 +  type T = (string * term list) list delayed;
    1.34 +  val empty = Ready [];
    1.35    val extend = I;
    1.36    fun merge _ = ToDo;
    1.37  );
    1.38 @@ -228,15 +226,14 @@
    1.39    then error "Roundup bound exceeded (sublocale relation probably not terminating)."
    1.40    else
    1.41      let
    1.42 -      val {parameters = (_, params), dependencies, ...} = the_locale thy name;
    1.43 +      val dependencies = dependencies_of thy name;
    1.44        val instance = instance_of thy name morph;
    1.45      in
    1.46        if member (ident_eq thy) marked (name, instance)
    1.47        then (deps, marked)
    1.48        else
    1.49          let
    1.50 -          val dependencies' =
    1.51 -            map (fn ((name, morph'), _) => (name, morph' $>  morph)) dependencies;
    1.52 +          val dependencies' = map (fn (name, morph') => (name, morph' $> morph)) dependencies;
    1.53            val marked' = (name, instance) :: marked;
    1.54            val (deps', marked'') = fold_rev (add thy (depth + 1)) dependencies' ([], marked');
    1.55          in
    1.56 @@ -250,7 +247,7 @@
    1.57    let
    1.58      (* Find all dependencies incuding new ones (which are dependencies enriching
    1.59        existing registrations). *)
    1.60 -    val (dependencies, marked') = add thy 0 (name, morph) ([], empty);
    1.61 +    val (dependencies, marked') = add thy 0 (name, morph) ([], []);
    1.62      (* Filter out exisiting fragments. *)
    1.63      val dependencies' = filter_out (fn (name, morph) =>
    1.64        member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies;
    1.65 @@ -348,7 +345,7 @@
    1.66  
    1.67  fun init name thy =
    1.68    activate_all name thy init_local_elem (Element.transfer_morphism o ProofContext.theory_of)
    1.69 -    (empty, ProofContext.init thy) |-> put_local_idents;
    1.70 +    ([], ProofContext.init thy) |-> put_local_idents;
    1.71  
    1.72  fun print_locale thy show_facts name =
    1.73    let
    1.74 @@ -357,7 +354,7 @@
    1.75    in
    1.76      Pretty.big_list "locale elements:"
    1.77        (activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy))
    1.78 -        (empty, []) |> snd |> rev |>
    1.79 +        ([], []) |> snd |> rev |>
    1.80          map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
    1.81    end
    1.82