src/Pure/Isar/class_target.ML
changeset 32074 76d6ba08a05f
parent 31988 801aabf9f376
child 32379 a97e9caebd60
child 32800 57fcca4e7c0e
     1.1 --- a/src/Pure/Isar/class_target.ML	Wed Jul 15 10:11:13 2009 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Wed Jul 15 18:20:08 2009 +0200
     1.3 @@ -242,15 +242,16 @@
     1.4      val diff_sort = Sign.complete_sort thy [sup]
     1.5        |> subtract (op =) (Sign.complete_sort thy [sub])
     1.6        |> filter (is_class thy);
     1.7 -    val deps_witss = case some_dep_morph
     1.8 -     of SOME dep_morph => [((sup, dep_morph), the_list some_wit)]
     1.9 -      | NONE => []
    1.10 +    val add_dependency = case some_dep_morph
    1.11 +     of SOME dep_morph => Locale.add_dependency sub
    1.12 +          (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export
    1.13 +      | NONE => I
    1.14    in
    1.15      thy
    1.16      |> AxClass.add_classrel classrel
    1.17      |> ClassData.map (Graph.add_edge (sub, sup))
    1.18      |> activate_defs sub (these_defs thy diff_sort)
    1.19 -    |> Locale.add_dependencies sub deps_witss export
    1.20 +    |> add_dependency
    1.21    end;
    1.22  
    1.23