--- a/src/Pure/Isar/class.ML Mon Sep 24 11:50:09 2018 +0200
+++ b/src/Pure/Isar/class.ML Mon Sep 24 11:58:07 2018 +0200
@@ -488,7 +488,7 @@
val diff_sort = Sign.complete_sort thy [sup]
|> subtract (op =) (Sign.complete_sort thy [sub])
|> filter (is_class thy);
- fun add_dependency some_wit (* FIXME unused!? *) =
+ val add_dependency =
(case some_dep_morph of
SOME dep_morph =>
Generic_Target.locale_dependency sub
@@ -501,7 +501,7 @@
(Axclass.add_classrel classrel
#> Class_Data.map (Graph.add_edge (sub, sup))
#> activate_defs sub (these_defs thy diff_sort))
- |> add_dependency some_witn
+ |> add_dependency
|> synchronize_class_syntax_target sub
end;