src/Pure/Tools/rule_insts.ML

--- a/src/Pure/Tools/rule_insts.ML	Thu Sep 09 14:05:31 2021 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Thu Sep 09 14:50:26 2021 +0200
@@ -53,7 +53,7 @@
   error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos);
 
 fun the_sort tvars (ai, pos) : sort =
-  (case TVars.get_first (fn ((bi, S), ()) => if ai = bi then SOME S else NONE) tvars of
+  (case TVars.get_first (fn ((bi, S), _) => if ai = bi then SOME S else NONE) tvars of
     SOME S => S
   | NONE => error_var "No such type variable in theorem: " (ai, pos));
 
@@ -128,7 +128,7 @@
     val instT1 =
       Term_Subst.instantiateT (TVars.make (map (read_type ctxt1 tvars) type_insts));
     val vars1 =
-      Vartab.build (vars |> Vars.fold (fn ((v, T), ()) =>
+      Vartab.build (vars |> Vars.fold (fn ((v, T), _) =>
         Vartab.insert (K true) (v, instT1 T)));
 
     (*term instantiations*)