diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML	Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML	Sat Nov 30 22:33:21 2024 +0100
@@ -87,7 +87,7 @@
 
 fun Mset ctxt prop =
   let
-    val [(Mset, _), (P, _)] = Variable.variant_frees ctxt [] [("Mset", ()), ("P", ())];
+    val [(Mset, _), (P, _)] = Variable.variant_names ctxt [("Mset", ()), ("P", ())];
 
     val vars = get_vars prop;
     val varsT = fastype_of (mk_bodyC vars);