src/Pure/more_thm.ML

--- a/src/Pure/more_thm.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/more_thm.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -25,8 +25,8 @@
   structure Thmtab: TABLE
   val eq_ctyp: ctyp * ctyp -> bool
   val aconvc: cterm * cterm -> bool
-  val add_tvars: thm -> ctyp Term_Subst.TVars.table -> ctyp Term_Subst.TVars.table
-  val add_vars: thm -> cterm Term_Subst.Vars.table -> cterm Term_Subst.Vars.table
+  val add_tvars: thm -> ctyp TVars.table -> ctyp TVars.table
+  val add_vars: thm -> cterm Vars.table -> cterm Vars.table
   val dest_funT: ctyp -> ctyp * ctyp
   val strip_type: ctyp -> ctyp list * ctyp
   val all_name: Proof.context -> string * cterm -> cterm -> cterm
@@ -140,12 +140,12 @@
 val add_tvars =
   Thm.fold_atomic_ctyps {hyps = false} Term.is_TVar (fn cT => fn tab =>
     let val v = Term.dest_TVar (Thm.typ_of cT)
-    in tab |> not (Term_Subst.TVars.defined tab v) ? Term_Subst.TVars.update (v, cT) end);
+    in tab |> not (TVars.defined tab v) ? TVars.add (v, cT) end);
 
 val add_vars =
   Thm.fold_atomic_cterms {hyps = false} Term.is_Var (fn ct => fn tab =>
     let val v = Term.dest_Var (Thm.term_of ct)
-    in tab |> not (Term_Subst.Vars.defined tab v) ? Term_Subst.Vars.update (v, ct) end);
+    in tab |> not (Vars.defined tab v) ? Vars.add (v, ct) end);
 
 
 (* ctyp operations *)
@@ -414,8 +414,8 @@
         val idx = Thm.maxidx_of th + 1;
         fun index ((a, A), b) = (((a, idx), A), b);
         val insts = (map index instT, map index inst);
-        val tfrees = Symtab.build (fold (Symtab.insert_set o #1 o #1) instT);
-        val frees = Symtab.build (fold (Symtab.insert_set o #1 o #1) inst);
+        val tfrees = Names.build (fold (Names.add_set o #1 o #1) instT);
+        val frees = Names.build (fold (Names.add_set o #1 o #1) inst);
 
         val hyps = Thm.chyps_of th;
         val inst_cterm =
@@ -454,11 +454,11 @@
 fun forall_intr_vars th =
   let
     val (_, vars) =
-      (th, (Term_Subst.Vars.empty, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Var
+      (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 (Term_Subst.Vars.defined seen v)
-            then (Term_Subst.Vars.add (v, ()) seen, ct :: vars)
+            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;
@@ -466,15 +466,15 @@
 fun forall_intr_frees th =
   let
     val fixed =
-      Term_Subst.Frees.build
-       (fold Term_Subst.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #>
-        fold Term_Subst.add_frees (Thm.hyps_of th));
+      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 (Term_Subst.Frees.defined seen v)
-            then (Term_Subst.Frees.add (v, ()) seen, ct :: frees)
+            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;
@@ -492,23 +492,23 @@
     val certT = Thm.global_ctyp_of thy;
 
     val instT =
-      Term_Subst.TVars.build (prop |> (Term.fold_types o Term.fold_atyps)
+      TVars.build (prop |> (Term.fold_types o Term.fold_atyps)
         (fn T => fn instT =>
           (case T of
             TVar (v as ((a, _), S)) =>
-              if Term_Subst.TVars.defined instT v then instT
-              else Term_Subst.TVars.update (v, TFree (a, S)) instT
+              if TVars.defined instT v then instT
+              else TVars.add (v, TFree (a, S)) instT
           | _ => instT)));
-    val cinstT = Term_Subst.TVars.map (K certT) instT;
+    val cinstT = TVars.map (K certT) instT;
     val cinst =
-      Term_Subst.Vars.build (prop |> Term.fold_aterms
+      Vars.build (prop |> Term.fold_aterms
         (fn t => fn inst =>
           (case t of
             Var ((x, i), T) =>
               let val T' = Term_Subst.instantiateT instT T
-              in Term_Subst.Vars.update (((x, i), T'), cert (Free ((x, T')))) inst end
+              in Vars.add (((x, i), T'), cert (Free ((x, T')))) inst end
           | _ => inst)));
-  in Thm.instantiate (Term_Subst.TVars.dest cinstT, Term_Subst.Vars.dest cinst) th end;
+  in Thm.instantiate (TVars.dest cinstT, Vars.dest cinst) th end;
 
 fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy;