--- a/src/HOL/ex/Cartouche_Examples.thy Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy Mon Nov 03 14:50:27 2014 +0100
@@ -36,7 +36,7 @@
subsection {* Outer syntax: cartouche within command syntax *}
ML {*
- Outer_Syntax.improper_command @{command_spec "cartouche"} ""
+ Outer_Syntax.command @{command_spec "cartouche"} ""
(Parse.cartouche >> (fn s =>
Toplevel.imperative (fn () => writeln s)))
*}
@@ -112,7 +112,7 @@
subsubsection {* Term cartouche and regular quotes *}
ML {*
- Outer_Syntax.improper_command @{command_spec "term_cartouche"} ""
+ Outer_Syntax.command @{command_spec "term_cartouche"} ""
(Parse.inner_syntax Parse.cartouche >> (fn s =>
Toplevel.keep (fn state =>
let