src/Pure/variable.ML

--- a/src/Pure/variable.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/variable.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -69,15 +69,15 @@
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_morphism: Proof.context -> Proof.context -> morphism
   val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
-  val importT_inst: term list -> Proof.context -> typ Term_Subst.TVars.table * Proof.context
+  val importT_inst: term list -> Proof.context -> typ TVars.table * Proof.context
   val import_inst: bool -> term list -> Proof.context ->
-    (typ Term_Subst.TVars.table * term Term_Subst.Vars.table) * Proof.context
+    (typ TVars.table * term Vars.table) * Proof.context
   val importT_terms: term list -> Proof.context -> term list * Proof.context
   val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
-  val importT: thm list -> Proof.context -> (ctyp Term_Subst.TVars.table * thm list) * Proof.context
+  val importT: thm list -> Proof.context -> (ctyp TVars.table * thm list) * Proof.context
   val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
   val import: bool -> thm list -> Proof.context ->
-    ((ctyp Term_Subst.TVars.table * cterm Term_Subst.Vars.table) * thm list) * Proof.context
+    ((ctyp TVars.table * cterm Vars.table) * thm list) * Proof.context
   val import_vars: Proof.context -> thm -> thm
   val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
@@ -515,14 +515,14 @@
     val still_fixed = not o is_newly_fixed inner outer;
 
     val gen_fixes =
-      Symtab.build (fixes_of inner |> Name_Space.fold_table (fn (y, _) =>
-        not (is_fixed outer y) ? Symtab.insert_set y));
+      Names.build (fixes_of inner |> Name_Space.fold_table (fn (y, _) =>
+        not (is_fixed outer y) ? Names.add_set y));
 
     val type_occs_inner = type_occs_of inner;
     fun gen_fixesT ts =
-      Symtab.build (fold decl_type_occs ts type_occs_inner |> Symtab.fold (fn (a, xs) =>
+      Names.build (fold decl_type_occs ts type_occs_inner |> Symtab.fold (fn (a, xs) =>
         if declared_outer a orelse exists still_fixed xs
-        then I else Symtab.insert_set a));
+        then I else Names.add_set a));
   in (gen_fixesT, gen_fixes) end;
 
 fun exportT_inst inner outer = #1 (export_inst inner outer);
@@ -533,7 +533,7 @@
     val maxidx = maxidx_of outer;
   in
     fn ts => ts |> map
-      (Term_Subst.generalize (mk_tfrees ts, Symtab.empty)
+      (Term_Subst.generalize (mk_tfrees ts, Names.empty)
         (fold (Term.fold_types Term.maxidx_typ) ts maxidx + 1))
   end;
 
@@ -564,7 +564,7 @@
     val idx = fold Thm.maxidx_thm ths maxidx + 1;
   in map (Thm.generalize (tfrees, frees) idx) ths end;
 
-fun exportT inner outer = gen_export (exportT_inst inner outer, Symtab.empty) (maxidx_of outer);
+fun exportT inner outer = gen_export (exportT_inst inner outer, Names.empty) (maxidx_of outer);
 fun export inner outer = gen_export (export_inst inner outer) (maxidx_of outer);
 
 fun export_morphism inner outer =
@@ -592,9 +592,7 @@
   let
     val tvars = build_rev (fold Term.add_tvars ts);
     val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt;
-    val instT =
-      Term_Subst.TVars.build (fold2 (fn a => fn b =>
-        Term_Subst.TVars.add (a, TFree b)) tvars tfrees);
+    val instT = TVars.build (fold2 (fn a => fn b => TVars.add (a, TFree b)) tvars tfrees);
   in (instT, ctxt') end;
 
 fun import_inst is_open ts ctxt =
@@ -603,14 +601,12 @@
     val (instT, ctxt') = importT_inst ts ctxt;
     val vars = map (apsnd (Term_Subst.instantiateT instT)) (build_rev (fold Term.add_vars ts));
     val (ys, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';
-    val inst =
-      Term_Subst.Vars.build (fold2 (fn (x, T) => fn y =>
-        Term_Subst.Vars.add ((x, T), Free (y, T))) vars ys);
+    val inst = Vars.build (fold2 (fn (x, T) => fn y => Vars.add ((x, T), Free (y, T))) vars ys);
   in ((instT, inst), ctxt'') end;
 
 fun importT_terms ts ctxt =
   let val (instT, ctxt') = importT_inst ts ctxt
-  in (map (Term_Subst.instantiate (instT, Term_Subst.Vars.empty)) ts, ctxt') end;
+  in (map (Term_Subst.instantiate (instT, Vars.empty)) ts, ctxt') end;
 
 fun import_terms is_open ts ctxt =
   let val (inst, ctxt') = import_inst is_open ts ctxt
@@ -619,8 +615,8 @@
 fun importT ths ctxt =
   let
     val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
-    val instT' = Term_Subst.TVars.map (K (Thm.ctyp_of ctxt')) instT;
-    val ths' = map (Thm.instantiate (Term_Subst.TVars.dest instT', [])) ths;
+    val instT' = TVars.map (K (Thm.ctyp_of ctxt')) instT;
+    val ths' = map (Thm.instantiate (TVars.dest instT', [])) ths;
   in ((instT', ths'), ctxt') end;
 
 fun import_prf is_open prf ctxt =
@@ -632,9 +628,9 @@
 fun import is_open ths ctxt =
   let
     val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
-    val instT' = Term_Subst.TVars.map (K (Thm.ctyp_of ctxt')) instT;
-    val inst' = Term_Subst.Vars.map (K (Thm.cterm_of ctxt')) inst;
-    val ths' = map (Thm.instantiate (Term_Subst.TVars.dest instT', Term_Subst.Vars.dest inst')) ths;
+    val instT' = TVars.map (K (Thm.ctyp_of ctxt')) instT;
+    val inst' = Vars.map (K (Thm.cterm_of ctxt')) inst;
+    val ths' = map (Thm.instantiate (TVars.dest instT', Vars.dest inst')) ths;
   in (((instT', inst'), ths'), ctxt') end;
 
 fun import_vars ctxt th =
@@ -690,10 +686,10 @@
 
 fun focus_subgoal bindings i st =
   let
-    val all_vars = Term_Subst.Vars.build (Thm.fold_terms {hyps = false} Term_Subst.add_vars st);
+    val all_vars = Vars.build (Thm.fold_terms {hyps = false} Vars.add_vars st);
   in
-    Term_Subst.Vars.fold (unbind_term o #1 o #1) all_vars #>
-    Term_Subst.Vars.fold (declare_constraints o Var o #1) all_vars #>
+    Vars.fold (unbind_term o #1 o #1) all_vars #>
+    Vars.fold (declare_constraints o Var o #1) all_vars #>
     focus_cterm bindings (Thm.cprem_of st i)
   end;
 
@@ -732,14 +728,14 @@
     val occs = type_occs_of ctxt;
     val occs' = type_occs_of ctxt';
     val types =
-      Symtab.build (occs' |> Symtab.fold (fn (a, _) =>
-        if Symtab.defined occs a then I else Symtab.insert_set a));
+      Names.build (occs' |> Symtab.fold (fn (a, _) =>
+        if Symtab.defined occs a then I else Names.add_set a));
     val idx = maxidx_of ctxt' + 1;
     val Ts' = (fold o fold_types o fold_atyps)
       (fn T as TFree _ =>
           (case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v | _ => I)
         | _ => I) ts [];
-    val ts' = map (Term_Subst.generalize (types, Symtab.empty) idx) ts;
+    val ts' = map (Term_Subst.generalize (types, Names.empty) idx) ts;
   in (rev Ts', ts') end;
 
 fun polymorphic ctxt ts = snd (polymorphic_types ctxt ts);