# HG changeset patch
# User wenzelm
# Date 1631218325 -7200
# Node ID a123db647573d9ef7f43ea2dcf4a5bfbc8441e90
# Parent  8cff7900871f28c4eebd0fed00eeeba2606bc4ce
clarified signature;
tuned;

diff -r 8cff7900871f -r a123db647573 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 ()
diff -r 8cff7900871f -r a123db647573 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu Sep 09 21:44:11 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu Sep 09 22:12:05 2021 +0200
@@ -97,8 +97,8 @@
 
     val type_tfrees = TFrees.build (TFrees.add_tfreesT (Term.fastype_of u));
     val extra_tfrees =
-      build_rev (u |> (Term.fold_types o Term.fold_atyps)
-        (fn TFree v => not (TFrees.defined type_tfrees v) ? insert (op =) v | _ => I));
+      TFrees.build (TFrees.add_tfrees_unless (TFrees.defined type_tfrees) u)
+      |> TFrees.list_set;
     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
   in (global_rhs, (extra_tfrees, (type_params, term_params))) end;
 
@@ -263,8 +263,8 @@
     val T = Term.fastype_of rhs;
     val type_tfrees = TFrees.build (TFrees.add_tfreesT T #> fold (TFrees.add_tfreesT o #2) xs);
     val extra_tfrees =
-      build_rev (rhs |> (Term.fold_types o Term.fold_atyps)
-        (fn TFree v => not (TFrees.defined type_tfrees v) ? insert (op =) v | _ => I));
+      TFrees.build (rhs |> TFrees.add_tfrees_unless (TFrees.defined type_tfrees))
+      |> TFrees.list_set;
     val mx' = check_mixfix lthy (b, extra_tfrees) mx;
 
     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
diff -r 8cff7900871f -r a123db647573 src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Thu Sep 09 21:44:11 2021 +0200
+++ b/src/Pure/primitive_defs.ML	Thu Sep 09 22:12:05 2021 +0200
@@ -51,9 +51,10 @@
     val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
       if check_free_rhs x orelse member (op aconv) args v then I
       else insert (op aconv) v | _ => I) rhs [];
-    val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
-      if check_tfree a orelse TFrees.defined head_tfrees (a, S) then I
-      else insert (op =) v | _ => I)) rhs [];
+    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;
   in
     if not (check_head head) then
       err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head])
diff -r 8cff7900871f -r a123db647573 src/Pure/term_items.ML
--- a/src/Pure/term_items.ML	Thu Sep 09 21:44:11 2021 +0200
+++ b/src/Pure/term_items.ML	Thu Sep 09 22:12:05 2021 +0200
@@ -96,6 +96,8 @@
   include TERM_ITEMS
   val add_tfreesT: typ -> set -> set
   val add_tfrees: term -> set -> set
+  val add_tfreesT_unless: (string * sort -> bool) -> typ -> set -> set
+  val add_tfrees_unless: (string * sort -> bool) -> term -> set -> set
 end =
 struct
 
@@ -109,6 +111,9 @@
 val add_tfreesT = fold_atyps (fn TFree v => add_set v | _ => I);
 val add_tfrees = fold_types add_tfreesT;
 
+fun add_tfreesT_unless pred = Term.fold_atyps (fn TFree v => not (pred v) ? add_set v | _ => I);
+fun add_tfrees_unless pred = fold_types (add_tfreesT_unless pred);
+
 end;
 
 
diff -r 8cff7900871f -r a123db647573 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Sep 09 21:44:11 2021 +0200
+++ b/src/Pure/theory.ML	Thu Sep 09 22:12:05 2021 +0200
@@ -244,10 +244,10 @@
         [] => (item, map Logic.varifyT_global args)
       | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, []));
 
-    val lhs_vars = TFrees.build (snd lhs |> fold TFrees.add_tfreesT);
+    val lhs_vars = TFrees.build (fold TFrees.add_tfreesT (snd lhs));
     val rhs_extras =
-      build (rhs |> fold (#2 #> (fold o Term.fold_atyps)
-        (fn TFree v => not (TFrees.defined lhs_vars v) ? insert (op =) v | _ => I)));
+      TFrees.build (rhs |> fold (fold (TFrees.add_tfreesT_unless (TFrees.defined lhs_vars)) o snd))
+      |> TFrees.list_set_rev;
     val _ =
       if null rhs_extras then ()
       else error ("Specification depends on extra type variables: " ^