src/Pure/drule.ML

--- a/src/Pure/drule.ML	Sun Sep 05 23:21:32 2021 +0200
+++ b/src/Pure/drule.ML	Mon Sep 06 11:32:18 2021 +0200
@@ -184,7 +184,7 @@
       |> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T));
     val Ts = map Term.fastype_of ps;
     val inst =
-      Term_Subst.Vars.build (th |> (Thm.fold_terms o Term.fold_aterms)
+      Term_Subst.Vars.build (th |> (Thm.fold_terms {hyps = false} o Term.fold_aterms)
         (fn t => fn inst =>
           (case t of
             Var (xi, T) =>