--- a/src/Pure/Isar/class_target.ML Fri Jul 10 07:59:28 2009 +0200
+++ b/src/Pure/Isar/class_target.ML Fri Jul 10 07:59:29 2009 +0200
@@ -242,16 +242,15 @@
val diff_sort = Sign.complete_sort thy [sup]
|> subtract (op =) (Sign.complete_sort thy [sub])
|> filter (is_class thy);
+ val deps_witss = case some_dep_morph
+ of SOME dep_morph => [((sup, dep_morph), the_list some_wit)]
+ | NONE => []
in
thy
|> AxClass.add_classrel classrel
|> ClassData.map (Graph.add_edge (sub, sup))
|> activate_defs sub (these_defs thy diff_sort)
- |> fold (fn dep_morph => Locale.add_dependency sub (sup,
- dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export))
- (the_list some_dep_morph)
- |> (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
- (Locale.get_registrations thy) thy)
+ |> Locale.add_dependencies sub deps_witss export
end;