diff -r f012cbfd96d0 -r cdc43c0fdbfc src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Sat Nov 30 22:02:36 2024 +0100
+++ b/src/Pure/Isar/object_logic.ML	Sat Nov 30 22:33:21 2024 +0100
@@ -159,7 +159,7 @@
 
 fun is_propositional ctxt T =
   T = propT orelse
-    let val x = Free (singleton (Variable.variant_frees ctxt []) ("x", T))
+    let val x = Free (singleton (Variable.variant_names ctxt) ("x", T))
     in can (fn () => Syntax.check_term ctxt (ensure_propT ctxt x)) () end;