src/Pure/Isar/locale.ML
changeset 37104 3877a6c45d57
parent 37103 6ea25bb157e1
child 37105 e464f84f3680
     1.1 --- a/src/Pure/Isar/locale.ML	Mon May 24 10:48:32 2010 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon May 24 10:48:32 2010 +0200
     1.3 @@ -330,7 +330,7 @@
     1.4  
     1.5  structure Registrations = Theory_Data
     1.6  (
     1.7 -  type T = ((string * (morphism * morphism)) * serial) list *
     1.8 +  type T = (((string * term list) * (morphism * morphism)) * serial) list *
     1.9      (* registrations, in reverse order of declaration;
    1.10         serial points to mixin list *)
    1.11      (serial * ((morphism * bool) * serial) list) list;
    1.12 @@ -348,8 +348,8 @@
    1.13  
    1.14  (* Primitive operations *)
    1.15  
    1.16 -fun add_reg export (dep, morph) =
    1.17 -  Registrations.map (apfst (cons ((dep, (morph, export)), serial ())));
    1.18 +fun add_reg thy export (name, morph) =
    1.19 +  Registrations.map (apfst (cons (((name, instance_of thy name (morph $> export)), (morph, export)), serial ())));
    1.20  
    1.21  fun add_mixin serial' mixin =
    1.22    (* registration to be amended identified by its serial id *)
    1.23 @@ -359,8 +359,8 @@
    1.24    let
    1.25      val (regs, mixins) = Registrations.get thy;
    1.26    in
    1.27 -    case find_first (fn ((name', (morph', export')), _) => ident_eq
    1.28 -      ((name', instance_of thy name' (morph' $> export')), (name, instance_of thy name morph))) (rev regs) of
    1.29 +    case find_first (fn (((name', inst'), (morph', export')), _) => ident_eq
    1.30 +      ((name', inst'), (name, instance_of thy name morph))) (rev regs) of
    1.31        NONE => []
    1.32      | SOME (_, serial) => the_default [] (AList.lookup (op =) mixins serial)
    1.33    end;
    1.34 @@ -379,14 +379,14 @@
    1.35    in (name, base $> mix $> export) end;
    1.36  
    1.37  fun these_registrations thy name = Registrations.get thy
    1.38 -  |>> filter (curry (op =) name o fst o fst)
    1.39 +  |>> filter (curry (op =) name o fst o fst o fst)
    1.40    (* with inherited mixins *)
    1.41 -  |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
    1.42 +  |-> (fn regs => fn _ => map (fn (((name, _), (base, export)) ,_) =>
    1.43      (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
    1.44  
    1.45  fun all_registrations thy = Registrations.get thy (* FIXME clone *)
    1.46    (* with inherited mixins *)
    1.47 -  |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
    1.48 +  |-> (fn regs => fn _ => map (fn (((name, _), (base, export)) ,_) =>
    1.49      (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
    1.50  
    1.51  fun activate_notes' activ_elem transfer thy export (name, morph) input =
    1.52 @@ -446,8 +446,7 @@
    1.53    let
    1.54      val regs = Registrations.get thy |> fst;
    1.55      val base = instance_of thy name (morph $> export);
    1.56 -    fun match ((name', (morph', export')), _) =
    1.57 -      ident_eq ((name, base), (name', instance_of thy name' (morph' $> export)));
    1.58 +    fun match (((name', inst'), _), _) = ident_eq ((name, base), (name', inst'));
    1.59    in
    1.60      case find_first match (rev regs) of
    1.61          NONE => error ("No interpretation of locale " ^
    1.62 @@ -472,7 +471,7 @@
    1.63      else
    1.64        (get_idents (Context.Theory thy), thy)
    1.65        (* add new registrations with inherited mixins *)
    1.66 -      |> roundup thy (add_reg export) export (name, morph)
    1.67 +      |> roundup thy (add_reg thy export) export (name, morph)
    1.68        |> snd
    1.69        (* add mixin *)
    1.70        |> (case mixin of NONE => I