--- 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 ()
--- 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;
--- 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])
--- 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;
--- 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: " ^