| changeset 81519 | cdc43c0fdbfc |
| parent 74561 | 8e6c973003c8 |
| child 82641 | d22294b20573 |
--- 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;