changeset 56072 | 31e427387ab5 |
parent 55828 | 42ac3cfb89f6 |
child 56275 | 600f432ab556 |
--- a/src/HOL/ex/Cartouche_Examples.thy Wed Mar 12 22:44:55 2014 +0100 +++ b/src/HOL/ex/Cartouche_Examples.thy Wed Mar 12 22:57:50 2014 +0100 @@ -106,7 +106,7 @@ setup -- "ML antiquotation" {* - ML_Antiquote.inline @{binding term_cartouche} + ML_Antiquotation.inline @{binding term_cartouche} (Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >> (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s)))) *}