changeset 81545 | 6f8a56a6b391 |
parent 81543 | fa37ee54644c |
--- a/src/Pure/variable.ML Fri Dec 06 15:20:43 2024 +0100 +++ b/src/Pure/variable.ML Fri Dec 06 20:26:33 2024 +0100 @@ -705,7 +705,7 @@ fun focus_params bindings t ctxt = let - val ps = Term.variant_bounds t (Term.strip_all_vars t); + val ps = Syntax_Trans.variant_bounds ctxt t (Term.strip_all_vars t); val (xs, Ts) = split_list ps; val (xs', ctxt') = (case bindings of