clarified set of items with order of addition;

--- a/src/HOL/Analysis/metric_arith.ML	Thu Sep 09 14:05:31 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML	Thu Sep 09 14:50:26 2021 +0200
@@ -24,7 +24,7 @@
 fun IF_UNSOLVED' tac i = IF_UNSOLVED (tac i)
 fun REPEAT' tac i = REPEAT (tac i)
 
-fun free_in v ct = member (op aconvc) (Misc_Legacy.cterm_frees ct) v
+fun free_in v ct = Cterms.defined (Misc_Legacy.cterm_frees ct) v
 
 (* build a cterm set with elements cts of type ty *)
 fun mk_ct_set ctxt ty =

--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Sep 09 14:05:31 2021 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Sep 09 14:50:26 2021 +0200
@@ -206,7 +206,8 @@
    val pcv = Simplifier.rewrite (put_simpset ss' ctxt);
    val postcv = Simplifier.rewrite (put_simpset ss ctxt);
    val nnf = K (nnf_conv ctxt then_conv postcv)
-   val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Misc_Legacy.cterm_frees tm)
+   val env = Cterms.list_set_rev (Misc_Legacy.cterm_frees tm)
+   val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons env
                   (isolate_conv ctxt) nnf
                   (fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt,
                                                whatis = whatis, simpset = ss}) vs

--- a/src/HOL/Decision_Procs/langford.ML	Thu Sep 09 14:05:31 2021 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Thu Sep 09 14:50:26 2021 +0200
@@ -185,10 +185,11 @@
       Simplifier.rewrite
         (put_simpset dlo_ss ctxt
           addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
+    val mk_env = Cterms.list_set_rev o Misc_Legacy.cterm_frees
   in
     fn p =>
       Qelim.gen_qelim_conv ctxt pcv pcv dnfex_conv cons
-        (Misc_Legacy.cterm_frees p) (K Thm.reflexive) (K Thm.reflexive)
+        (mk_env p) (K Thm.reflexive) (K Thm.reflexive)
         (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
   end;
 

--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Sep 09 14:05:31 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Sep 09 14:50:26 2021 +0200
@@ -860,18 +860,18 @@
   fun substitutable_monomial fvs tm =
     (case Thm.term_of tm of
       Free (_, \<^typ>\<open>real\<close>) =>
-        if not (member (op aconvc) fvs tm) then (@1, tm)
+        if not (Cterms.defined fvs tm) then (@1, tm)
         else raise Failure "substitutable_monomial"
     | \<^term>\<open>(*) :: real \<Rightarrow> _\<close> $ _ $ (Free _) =>
         if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso
-          not (member (op aconvc) fvs (Thm.dest_arg tm))
+          not (Cterms.defined fvs (Thm.dest_arg tm))
         then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm)
         else raise Failure "substitutable_monomial"
     | \<^term>\<open>(+) :: real \<Rightarrow> _\<close>$_$_ =>
-         (substitutable_monomial (merge (op aconvc) (fvs, Misc_Legacy.cterm_frees (Thm.dest_arg tm)))
+         (substitutable_monomial (fvs |> Cterms.fold Cterms.add (Misc_Legacy.cterm_frees (Thm.dest_arg tm)))
            (Thm.dest_arg1 tm)
            handle Failure _ =>
-            substitutable_monomial (merge (op aconvc) (fvs, Misc_Legacy.cterm_frees (Thm.dest_arg1 tm)))
+            substitutable_monomial (fvs |> Cterms.fold Cterms.add (Misc_Legacy.cterm_frees (Thm.dest_arg1 tm)))
               (Thm.dest_arg tm))
     | _ => raise Failure "substitutable_monomial")
 
@@ -898,7 +898,7 @@
 
     fun make_substitution th =
       let
-        val (c,v) = substitutable_monomial [] (Thm.dest_arg1(concl th))
+        val (c,v) = substitutable_monomial Cterms.empty (Thm.dest_arg1(concl th))
         val th1 =
           Drule.arg_cong_rule
             (Thm.apply \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close> (RealArith.cterm_of_rat (Rat.inv c)))

--- a/src/HOL/Tools/Qelim/qelim.ML	Thu Sep 09 14:05:31 2021 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Thu Sep 09 14:50:26 2021 +0200
@@ -65,8 +65,10 @@
 in
 
 fun standard_qelim_conv ctxt atcv ncv qcv p =
-  let val pcv = pcv ctxt
-  in gen_qelim_conv ctxt pcv pcv pcv cons (Misc_Legacy.cterm_frees p) atcv ncv qcv p end
+  let
+    val pcv = pcv ctxt
+    val env = Cterms.list_set_rev (Misc_Legacy.cterm_frees p)
+  in gen_qelim_conv ctxt pcv pcv pcv cons env atcv ncv qcv p end
 
 end;
 

--- a/src/HOL/Tools/groebner.ML	Thu Sep 09 14:05:31 2021 +0200
+++ b/src/HOL/Tools/groebner.ML	Thu Sep 09 14:50:26 2021 +0200
@@ -528,7 +528,7 @@
  fun simp_ex_conv ctxt =
    Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
 
-fun free_in v t = member op aconvc (Misc_Legacy.cterm_frees t) v;
+fun free_in v t = Cterms.defined (Misc_Legacy.cterm_frees t) v;
 
 val vsubst = let
  fun vsubst (t,v) tm =
@@ -737,7 +737,7 @@
       val all = Thm.cterm_of ctxt (Const (\<^const_name>\<open>All\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
     in Thm.apply all (Thm.lambda x p) end
   val avs = Misc_Legacy.cterm_frees tm
-  val P' = fold mk_forall avs tm
+  val P' = fold mk_forall (Cterms.list_set_rev avs) tm
   val th1 = initial_conv ctxt (mk_neg P')
   val (evs,bod) = strip_exists(concl th1) in
    if is_forall bod then raise CTERM("ring: non-universal formula",[tm])
@@ -752,7 +752,7 @@
       Thm.equal_elim
         (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [not_ex RS sym])
           (th2 |> Thm.cprop_of)) th2
-    in specl avs
+    in specl (Cterms.list_set_rev avs)
              ([[[HOLogic.mk_obj_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD)
    end
  end
@@ -795,7 +795,7 @@
    val mons = striplist(dest_binary ring_add_tm) t
   in member (op aconvc) mons v andalso
     forall (fn m => v aconvc m
-          orelse not(member (op aconvc) (Misc_Legacy.cterm_frees m) v)) mons
+          orelse not(Cterms.defined (Misc_Legacy.cterm_frees m) v)) mons
   end
 
   fun isolate_variable vars tm =
@@ -850,7 +850,7 @@
  fun isolate_monomials vars tm =
  let
   val (cmons,vmons) =
-    List.partition (fn m => null (inter (op aconvc) vars (Misc_Legacy.cterm_frees m)))
+    List.partition (fn m => null (inter (op aconvc) vars (Cterms.list_set_rev (Misc_Legacy.cterm_frees m))))
                    (striplist ring_dest_add tm)
   val cofactors = map (fn v => find_multipliers v vmons) vars
   val cnc = if null cmons then zero_tm

--- a/src/Pure/General/table.ML	Thu Sep 09 14:05:31 2021 +0200
+++ b/src/Pure/General/table.ML	Thu Sep 09 14:50:26 2021 +0200
@@ -25,7 +25,6 @@
   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
@@ -62,8 +61,6 @@
   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 =
@@ -124,7 +121,6 @@
           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 [];
 
@@ -450,9 +446,6 @@
 fun remove_set x : set -> set = delete_safe x;
 fun make_set xs = build (fold insert_set xs);
 
-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/Isar/obtain.ML	Thu Sep 09 14:05:31 2021 +0200
+++ b/src/Pure/Isar/obtain.ML	Thu Sep 09 14:50:26 2021 +0200
@@ -105,7 +105,7 @@
   let
     val frees = Frees.build (t |> Term.fold_aterms (fn Free v => Frees.add_set v | _ => I));
     val T =
-      (case Frees.get_first (fn ((x, T), ()) => if x = z then SOME T else NONE) frees of
+      (case Frees.get_first (fn ((x, T), _) => if x = z then SOME T else NONE) frees of
         SOME T => T
       | NONE => the_default dummyT (Variable.default_type ctxt z));
   in Logic.all_const T $ Term.lambda_name (y, Free (z, T)) t end;

--- a/src/Pure/Tools/rule_insts.ML	Thu Sep 09 14:05:31 2021 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Thu Sep 09 14:50:26 2021 +0200
@@ -53,7 +53,7 @@
   error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos);
 
 fun the_sort tvars (ai, pos) : sort =
-  (case TVars.get_first (fn ((bi, S), ()) => if ai = bi then SOME S else NONE) tvars of
+  (case TVars.get_first (fn ((bi, S), _) => if ai = bi then SOME S else NONE) tvars of
     SOME S => S
   | NONE => error_var "No such type variable in theorem: " (ai, pos));
 
@@ -128,7 +128,7 @@
     val instT1 =
       Term_Subst.instantiateT (TVars.make (map (read_type ctxt1 tvars) type_insts));
     val vars1 =
-      Vartab.build (vars |> Vars.fold (fn ((v, T), ()) =>
+      Vartab.build (vars |> Vars.fold (fn ((v, T), _) =>
         Vartab.insert (K true) (v, instT1 T)));
 
     (*term instantiations*)

--- a/src/Pure/goal.ML	Thu Sep 09 14:05:31 2021 +0200
+++ b/src/Pure/goal.ML	Thu Sep 09 14:50:26 2021 +0200
@@ -122,7 +122,7 @@
     val tfrees = TFrees.build (fold TFrees.add_tfrees (prop :: As));
     val Ts = Names.build (TFrees.fold (Names.add_set o #1 o #1) tfrees);
     val instT =
-      build (tfrees |> TFrees.fold (fn ((a, S), ()) =>
+      build (tfrees |> TFrees.fold (fn ((a, S), _) =>
         cons (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))));
 
     val global_prop =

--- a/src/Pure/more_thm.ML	Thu Sep 09 14:05:31 2021 +0200
+++ b/src/Pure/more_thm.ML	Thu Sep 09 14:50:26 2021 +0200
@@ -12,6 +12,7 @@
   val show_consts: bool Config.T
   val show_hyps: bool Config.T
   val show_tags: bool Config.T
+  structure Cterms: ITEMS
   structure Ctermtab: TABLE
   structure Thmtab: TABLE
   val aconvc: cterm * cterm -> bool
@@ -23,6 +24,7 @@
   include THM
   structure Ctermtab: TABLE
   structure Thmtab: TABLE
+  structure Cterms: ITEMS
   val eq_ctyp: ctyp * ctyp -> bool
   val aconvc: cterm * cterm -> bool
   val add_tvars: thm -> ctyp TVars.table -> ctyp TVars.table
@@ -220,6 +222,7 @@
 
 (* scalable collections *)
 
+structure Cterms = Items(type key = cterm val ord = fast_term_ord);
 structure Ctermtab = Table(type key = cterm val ord = fast_term_ord);
 structure Thmtab = Table(type key = thm val ord = thm_ord);
 
@@ -452,16 +455,8 @@
 (* implicit generalization over variables -- canonical order *)
 
 fun forall_intr_vars th =
-  let
-    val (_, vars) =
-      (th, (Vars.empty, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Var
-        (fn ct => fn (seen, vars) =>
-          let val v = Term.dest_Var (Thm.term_of ct) in
-            if not (Vars.defined seen v)
-            then (Vars.add_set v seen, ct :: vars)
-            else (seen, vars)
-          end);
-  in fold Thm.forall_intr vars th end;
+  let val vars = Cterms.build (Thm.fold_atomic_cterms {hyps = false} Term.is_Var Cterms.add_set th)
+  in fold_rev Thm.forall_intr (Cterms.list_set vars) th end;
 
 fun forall_intr_frees th =
   let
@@ -469,15 +464,11 @@
       Frees.build
        (fold Frees.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #>
         fold Frees.add_frees (Thm.hyps_of th));
-    val (_, frees) =
-      (th, (fixed, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Free
-        (fn ct => fn (seen, frees) =>
-          let val v = Term.dest_Free (Thm.term_of ct) in
-            if not (Frees.defined seen v)
-            then (Frees.add_set v seen, ct :: frees)
-            else (seen, frees)
-          end);
-  in fold Thm.forall_intr frees th end;
+    val is_fixed = Frees.defined fixed o Term.dest_Free o Thm.term_of;
+    val frees =
+      Cterms.build (th |> Thm.fold_atomic_cterms {hyps = false} Term.is_Free
+        (fn ct => not (is_fixed ct) ? Cterms.add_set ct));
+  in fold_rev Thm.forall_intr (Cterms.list_set frees) th end;
 
 
 (* unvarify_global: global schematic variables *)

--- a/src/Pure/term_ord.ML	Thu Sep 09 14:05:31 2021 +0200
+++ b/src/Pure/term_ord.ML	Thu Sep 09 14:50:26 2021 +0200
@@ -11,11 +11,11 @@
   type 'a table
   val empty: 'a table
   val build: ('a table -> 'a table) -> 'a table
+  val size: 'a table -> int
   val is_empty: 'a table -> bool
   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 exists: (key * 'a -> bool) -> 'a table -> bool
@@ -25,9 +25,11 @@
   val defined: 'a table -> key -> bool
   val add: key * 'a -> 'a table -> 'a table
   val make: (key * 'a) list -> 'a table
-  type set = unit table
+  type set = int table
   val add_set: key -> set -> set
   val make_set: key list -> set
+  val list_set: set -> key list
+  val list_set_rev: set -> key list
   val subset: set * set -> bool
   val eq_set: set * set -> bool
 end;
@@ -35,37 +37,55 @@
 functor Items(Key: KEY): ITEMS =
 struct
 
+(* table with length *)
+
 structure Table = Table(Key);
 
 type key = Table.key;
-type 'a table = 'a Table.table;
+datatype 'a table = Items of int * 'a Table.table;
+
+fun size (Items (n, _)) = n;
+fun table (Items (_, tab)) = tab;
+
+val empty = Items (0, Table.empty);
+fun build (f: 'a table -> 'a table) = f empty;
+fun is_empty items = size items = 0;
 
-val empty = Table.empty;
-val build = Table.build;
-val is_empty = Table.is_empty;
-val size = Table.size;
-val dest = Table.dest;
-val keys = Table.keys;
-val exists = Table.exists;
-val forall = Table.forall;
-val get_first = Table.get_first;
-val lookup = Table.lookup;
-val defined = Table.defined;
+fun dest items = Table.dest (table items);
+fun keys items = Table.keys (table items);
+fun exists pred = Table.exists pred o table;
+fun forall pred = Table.forall pred o table;
+fun get_first get = Table.get_first get o table;
+fun lookup items = Table.lookup (table items);
+fun defined items = Table.defined (table items);
+
+fun add (key, x) (items as Items (n, tab)) =
+  if Table.defined tab key then items
+  else Items (n + 1, Table.update_new (key, x) tab);
 
-fun add entry = Table.insert (K true) entry;
-fun make entries = Table.build (fold add entries);
+fun make entries = build (fold add entries);
+
+
+(* set with order of addition *)
 
-type set = unit table;
+type set = int table;
 
-fun add_set x = add (x, ());
+fun add_set x (items as Items (n, tab)) =
+  if Table.defined tab x then items
+  else Items (n + 1, Table.update_new (x, n) tab);
+
 fun make_set xs = build (fold add_set xs);
 
 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);
 
-val map = Table.map;
-val fold = Table.fold;
-val fold_rev = Table.fold_rev;
+fun list_set_ord ord items = Table.dest (table items) |> sort (ord o apply2 #2) |> map #1
+val list_set = list_set_ord int_ord;
+val list_set_rev = list_set_ord (rev_order o int_ord);
+
+fun map f (Items (n, tab)) = Items (n, Table.map f tab);
+fun fold f = Table.fold f o table;
+fun fold_rev f = Table.fold_rev f o table;
 
 end;
 

--- a/src/Tools/misc_legacy.ML	Thu Sep 09 14:05:31 2021 +0200
+++ b/src/Tools/misc_legacy.ML	Thu Sep 09 14:50:26 2021 +0200
@@ -5,8 +5,8 @@
 
 signature MISC_LEGACY =
 sig
-  val thm_frees: thm -> cterm list
-  val cterm_frees: cterm -> cterm list
+  val thm_frees: thm -> Cterms.set
+  val cterm_frees: cterm -> Cterms.set
   val add_term_names: term * string list -> string list
   val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   val add_term_tfrees: term * (string * sort) list -> (string * sort) list
@@ -26,16 +26,7 @@
 structure Misc_Legacy: MISC_LEGACY =
 struct
 
-fun thm_frees th =
-  (th, (Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true} Term.is_Free
-    (fn ct => fn (set, list) =>
-      let val v = Term.dest_Free (Thm.term_of ct) in
-        if not (Frees.defined set v)
-        then (Frees.add_set v set, ct :: list)
-        else (set, list)
-      end)
-  |> #2;
-
+val thm_frees = Cterms.build o Thm.fold_atomic_cterms {hyps = true} Term.is_Free Cterms.add_set;
 val cterm_frees = thm_frees o Drule.mk_term;
 
 (*iterate a function over all types in a term*)