src/Tools/code/code_wellsorted.ML

     val (classess, (superclasses, inst_params)) =
       obtain_instance thy arities inst;
   in
     vardeps_data
     |> (apsnd o apsnd) (insert (op =) inst)
-    |> fold_index (fn (k, classes) =>
-         apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))
-         ) classess
+    |> fold_index (fn (k, _) =>
+         apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))) classess
     |> fold (fn superclass => assert_inst thy arities eqngr (superclass, tyco)) superclasses
     |> fold (assert_fun thy arities eqngr) inst_params
     |> fold_index (fn (k, classes) =>
          add_classes thy arities eqngr (Inst (class, tyco), k) classes
          #> fold (fn superclass =>

     val ((lhs, rhss), eqns) = obtain_eqns thy eqngr c;
     val rhss' = (map o apsnd o map) (styp_of (SOME (c, lhs))) rhss;
   in
     vardeps_data
     |> (apsnd o apfst) (Symtab.update_new (c, (lhs, eqns)))
+    |> fold_index (fn (k, _) =>
+         apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))) lhs
     |> fold_index (fn (k, (_, sort)) =>
-         apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))
-         #> add_classes thy arities eqngr (Fun c, k) (complete_proper_sort thy sort)) lhs
+         add_classes thy arities eqngr (Fun c, k) (complete_proper_sort thy sort)) lhs
     |> fold (assert_rhs thy arities eqngr) rhss'
   end;
 
 
 (* applying instantiations *)