src/Pure/Isar/class_target.ML
changeset 31988 801aabf9f376
parent 31869 01fed718958c
child 32074 76d6ba08a05f
     1.1 --- a/src/Pure/Isar/class_target.ML	Fri Jul 10 07:59:28 2009 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Fri Jul 10 07:59:29 2009 +0200
     1.3 @@ -242,16 +242,15 @@
     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    in
    1.11      thy
    1.12      |> AxClass.add_classrel classrel
    1.13      |> ClassData.map (Graph.add_edge (sub, sup))
    1.14      |> activate_defs sub (these_defs thy diff_sort)
    1.15 -    |> fold (fn dep_morph => Locale.add_dependency sub (sup,
    1.16 -        dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export))
    1.17 -          (the_list some_dep_morph)
    1.18 -    |> (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
    1.19 -        (Locale.get_registrations thy) thy)
    1.20 +    |> Locale.add_dependencies sub deps_witss export
    1.21    end;
    1.22  
    1.23