--- a/src/Pure/thm.ML Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/thm.ML Sat Sep 04 21:25:08 2021 +0200
@@ -1641,8 +1641,8 @@
|> fold add_instT_sorts instT
|> fold add_inst_sorts inst;
- val instT' = fold (add_instT thy') instT Term_Subst.TVars.empty;
- val inst' = fold (add_inst thy') inst Term_Subst.Vars.empty;
+ val instT' = Term_Subst.TVars.build (fold (add_instT thy') instT);
+ val inst' = Term_Subst.Vars.build (fold (add_inst thy') inst);
in ((instT', inst'), (cert', sorts')) end;
in
@@ -2093,7 +2093,7 @@
val add_vars =
full_prop_of #>
fold_aterms (fn Var v => Vartab.insert_list (op =) v | _ => I);
- val vars = Vartab.empty |> add_vars th1 |> add_vars th2;
+ val vars = Vartab.build (add_vars th1 #> add_vars th2);
in SOME (Vartab.fold (unify_vars o #2) vars env) end
handle Pattern.Unif => NONE;