--- a/src/Pure/primitive_defs.ML	Thu Sep 09 22:12:05 2021 +0200
+++ b/src/Pure/primitive_defs.ML	Thu Sep 09 22:29:15 2021 +0200
@@ -54,7 +54,7 @@
     val rhs_extrasT =
       TFrees.build (rhs |> TFrees.add_tfrees_unless
         (fn (a, S) => check_tfree a orelse TFrees.defined head_tfrees (a, S)))
-      |> TFrees.list_set_rev |> map TFree;
+      |> TFrees.keys |> map TFree;
   in
     if not (check_head head) then
       err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head])