| changeset 67721 | 5348bea4accd |
| parent 64556 | 851ae0e7b09c |
| child 69575 | f77cc54f6d47 |
--- a/src/Pure/variable.ML Sun Feb 25 12:59:08 2018 +0100 +++ b/src/Pure/variable.ML Sun Feb 25 15:44:46 2018 +0100 @@ -642,7 +642,7 @@ val trade = gen_trade (import true) export; -(* focus on outermost parameters: !!x y z. B *) +(* focus on outermost parameters: \<And>x y z. B *) val bound_focus = Config.bool (Config.declare ("bound_focus", \<^here>) (K (Config.Bool false)));