--- a/src/Pure/Isar/obtain.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Isar/obtain.ML Thu Sep 09 12:33:14 2021 +0200
@@ -103,11 +103,9 @@
fun mk_all_internal ctxt (y, z) t =
let
- val frees =
- Term_Subst.Frees.build (t |> Term.fold_aterms
- (fn Free v => Term_Subst.Frees.add (v, ()) | _ => I));
+ val frees = Frees.build (t |> Term.fold_aterms (fn Free v => Frees.add_set v | _ => I));
val T =
- (case Term_Subst.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;
@@ -328,16 +326,16 @@
val terms = map (Drule.mk_term o Thm.cterm_of ctxt o Free) (xs @ ys');
val instT =
- Term_Subst.TVars.build
+ TVars.build
(params |> fold (#2 #> Term.fold_atyps (fn T => fn instT =>
(case T of
TVar v =>
- if Term_Subst.TVars.defined instT v then instT
- else Term_Subst.TVars.update (v, Thm.ctyp_of ctxt (norm_type T)) instT
+ if TVars.defined instT v then instT
+ else TVars.add (v, Thm.ctyp_of ctxt (norm_type T)) instT
| _ => instT))));
val closed_rule = rule
|> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var))
- |> Thm.instantiate (Term_Subst.TVars.dest instT, []);
+ |> Thm.instantiate (TVars.dest instT, []);
val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
val vars' =