--- a/src/Pure/variable.ML Sun Sep 05 23:21:32 2021 +0200
+++ b/src/Pure/variable.ML Mon Sep 06 11:32:18 2021 +0200
@@ -267,7 +267,7 @@
val declare_prf =
Proofterm.fold_proof_terms_types declare_internal (declare_internal o Logic.mk_type);
-val declare_thm = Thm.fold_terms declare_internal;
+val declare_thm = Thm.fold_terms {hyps = true} declare_internal;
(* renaming term/type frees *)
@@ -689,7 +689,9 @@
in ((xs ~~ ps', goal'), ctxt') end;
fun focus_subgoal bindings i st =
- let val all_vars = Term_Subst.Vars.build (Thm.fold_terms Term_Subst.add_vars st) in
+ let
+ val all_vars = Term_Subst.Vars.build (Thm.fold_terms {hyps = false} Term_Subst.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 #>
focus_cterm bindings (Thm.cprem_of st i)