diff -r 2ffdedb0c044 -r 31e427387ab5 src/HOL/ex/Cartouche_Examples.thy
--- 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))))
 *}