src/Pure/Isar/class.ML

       Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup))
         (fn {context = ctxt, ...} => EVERY (map (TRYALL o resolve_tac ctxt o single) intros));
     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
             {dep = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)),
               mixin = NONE, export = export}

     lthy
     |> Local_Theory.raw_theory
       (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;
 
 local