src/Pure/Isar/class.ML

     val diff_sort = Sign.complete_sort thy [sup]
       |> subtract (op =) (Sign.complete_sort thy [sub])
       |> filter (is_class thy);
     val add_dependency = case some_dep_morph
      of SOME dep_morph => Locale.add_dependency sub
-          (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export
+          (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) NONE export
       | NONE => I
   in
     thy
     |> AxClass.add_classrel classrel
     |> ClassData.map (Graph.add_edge (sub, sup))