src/Pure/variable.ML
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