src/Pure/Isar/expression.ML

--- a/src/Pure/Isar/expression.ML	Thu Sep 09 21:44:11 2021 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Sep 09 22:12:05 2021 +0200
@@ -698,8 +698,7 @@
     val Ts = map #2 xs;
     val type_tfrees = TFrees.build (fold TFrees.add_tfreesT Ts);
     val extra_tfrees =
-      TFrees.build (body |> (Term.fold_types o Term.fold_atyps)
-        (fn TFree v => not (TFrees.defined type_tfrees v) ? TFrees.add_set v | _ => I))
+      TFrees.build (TFrees.add_tfrees_unless (TFrees.defined type_tfrees) body)
       |> TFrees.list_set |> sort_by #1 |> map TFree;
     val predT = map Term.itselfT extra_tfrees ---> Ts ---> bodyT;
 
@@ -817,8 +816,7 @@
 
     val type_tfrees = TFrees.build (fold (TFrees.add_tfreesT o #2) parms);
     val extra_tfrees =
-      TFrees.build (exts' |> (fold o Term.fold_types o Term.fold_atyps)
-        (fn TFree v => not (TFrees.defined type_tfrees v) ? TFrees.add_set v | _ => I));
+      TFrees.build (fold (TFrees.add_tfrees_unless (TFrees.defined type_tfrees)) exts')
     val extraTs = TFrees.list_set_rev extra_tfrees;
     val _ =
       if null extraTs then ()