tuned -- removed spurious dead code from 7b9a67cbd48f;
authorwenzelm
Mon, 24 Sep 2018 11:58:07 +0200
changeset 69048 f79aeac59e15
parent 69047 17f9f50e2dbe
child 69049 1ad2897ba244
tuned -- removed spurious dead code from 7b9a67cbd48f;
src/Pure/Isar/class.ML
--- 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;