more scalable operations;

--- a/src/Pure/General/table.ML	Fri Sep 03 19:56:03 2021 +0200
+++ b/src/Pure/General/table.ML	Sat Sep 04 13:49:26 2021 +0200
@@ -24,13 +24,14 @@
   val map: (key -> 'a -> 'b) -> 'a table -> 'b table
   val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
   val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
+  val size: 'a table -> int
   val dest: 'a table -> (key * 'a) list
   val keys: 'a table -> key list
   val min: 'a table -> (key * 'a) option
   val max: 'a table -> (key * 'a) option
-  val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
   val exists: (key * 'a -> bool) -> 'a table -> bool
   val forall: (key * 'a -> bool) -> 'a table -> bool
+  val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
   val lookup_key: 'a table -> key -> (key * 'a) option
   val lookup: 'a table -> key -> 'a option
   val defined: 'a table -> key -> bool
@@ -60,6 +61,8 @@
   val insert_set: key -> set -> set
   val remove_set: key -> set -> set
   val make_set: key list -> set
+  val subset: set * set -> bool
+  val eq_set: set * set -> bool
 end;
 
 functor Table(Key: KEY): TABLE =
@@ -118,6 +121,7 @@
           fold left (f p1 (fold mid (f p2 (fold right x))));
   in fold end;
 
+fun size tab = fold_table (fn _ => fn n => n + 1) tab 0;
 fun dest tab = fold_rev_table cons tab [];
 fun keys tab = fold_rev_table (cons o #1) tab [];
 
@@ -137,6 +141,20 @@
   | max (Branch3 (_, _, _, _, right)) = max right;
 
 
+(* exists and forall *)
+
+fun exists pred =
+  let
+    fun ex Empty = false
+      | ex (Branch2 (left, (k, x), right)) =
+          ex left orelse pred (k, x) orelse ex right
+      | ex (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
+          ex left orelse pred (k1, x1) orelse ex mid orelse pred (k2, x2) orelse ex right;
+  in ex end;
+
+fun forall pred = not o exists (not o pred);
+
+
 (* get_first *)
 
 fun get_first f =
@@ -164,9 +182,6 @@
           | some => some);
   in get end;
 
-fun exists pred = is_some o get_first (fn entry => if pred entry then SOME () else NONE);
-fun forall pred = not o exists (not o pred);
-
 
 (* lookup *)
 
@@ -424,7 +439,7 @@
 fun merge_list eq = join (fn _ => Library.merge eq);
 
 
-(* unit tables *)
+(* set operations *)
 
 type set = unit table;
 
@@ -432,6 +447,9 @@
 fun remove_set x : set -> set = delete_safe x;
 fun make_set entries = fold insert_set entries empty;
 
+fun subset (A: set, B: set) = forall (defined B o #1) A;
+fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B);
+
 
 (* ML pretty-printing *)
 

--- a/src/Pure/raw_simplifier.ML	Fri Sep 03 19:56:03 2021 +0200
+++ b/src/Pure/raw_simplifier.ML	Sat Sep 04 13:49:26 2021 +0200
@@ -161,13 +161,13 @@
 fun rewrite_rule_extra_vars prems elhs erhs =
   let
     val elhss = elhs :: prems;
-    val tvars = fold Term.add_tvars elhss [];
-    val vars = fold Term.add_vars elhss [];
+    val tvars = fold Term_Subst.add_tvars elhss Term_Subst.TVars.empty;
+    val vars = fold Term_Subst.add_vars elhss Term_Subst.Vars.empty;
   in
     erhs |> Term.exists_type (Term.exists_subtype
-      (fn TVar v => not (member (op =) tvars v) | _ => false)) orelse
+      (fn TVar v => not (Term_Subst.TVars.defined tvars v) | _ => false)) orelse
     erhs |> Term.exists_subterm
-      (fn Var v => not (member (op =) vars v) | _ => false)
+      (fn Var v => not (Term_Subst.Vars.defined vars v) | _ => false)
   end;
 
 fun rrule_extra_vars elhs thm =
@@ -474,6 +474,8 @@
     (cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm));
       ctxt));
 
+fun vars_set t = Term_Subst.add_vars t Term_Subst.Vars.empty;
+
 local
 
 fun vperm (Var _, Var _) = true
@@ -481,8 +483,7 @@
   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
   | vperm (t, u) = (t = u);
 
-fun var_perm (t, u) =
-  vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
+fun var_perm (t, u) = vperm (t, u) andalso Term_Subst.Vars.eq_set (apply2 vars_set (t, u));
 
 in
 
@@ -945,7 +946,7 @@
   while the premises are solved.*)
 
 fun cond_skel (args as (_, (lhs, rhs))) =
-  if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
+  if Term_Subst.Vars.subset (vars_set rhs, vars_set lhs) then uncond_skel args
   else skel0;
 
 (*

--- a/src/Pure/term_subst.ML	Fri Sep 03 19:56:03 2021 +0200
+++ b/src/Pure/term_subst.ML	Sat Sep 04 13:49:26 2021 +0200
@@ -29,6 +29,15 @@
   structure TVars: INST_TABLE
   structure Frees: INST_TABLE
   structure Vars: INST_TABLE
+  val add_tfreesT: typ -> TFrees.set -> TFrees.set
+  val add_tfrees: term -> TFrees.set -> TFrees.set
+  val add_tvarsT: typ -> TVars.set -> TVars.set
+  val add_tvars: term -> TVars.set -> TVars.set
+  val add_frees: term -> Frees.set -> Frees.set
+  val add_vars: term -> Vars.set -> Vars.set
+  val add_tfree_namesT: typ -> Symtab.set -> Symtab.set
+  val add_tfree_names: term -> Symtab.set -> Symtab.set
+  val add_free_names: term -> Symtab.set -> Symtab.set
   val map_atypsT_same: typ Same.operation -> typ Same.operation
   val map_types_same: typ Same.operation -> term Same.operation
   val map_aterms_same: term Same.operation -> term Same.operation
@@ -77,6 +86,16 @@
   val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord)
 );
 
+val add_tfreesT = fold_atyps (fn TFree v => TFrees.add (v, ()) | _ => I);
+val add_tfrees = fold_types add_tfreesT;
+val add_tvarsT = fold_atyps (fn TVar v => TVars.add (v, ()) | _ => I);
+val add_tvars = fold_types add_tvarsT;
+val add_frees = fold_aterms (fn Free v => Frees.add (v, ()) | _ => I);
+val add_vars = fold_aterms (fn Var v => Vars.add (v, ()) | _ => I);
+val add_tfree_namesT = fold_atyps (fn TFree (a, _) => Symtab.insert_set a | _ => I);
+val add_tfree_names = fold_types add_tfree_namesT;
+val add_free_names = fold_aterms (fn Free (x, _) => Symtab.insert_set x | _ => I);
+
 
 (* generic mapping *)