changeset 58928 | 23d0ffd48006 |
parent 58893 | 9e0ecb66d6a7 |
child 58978 | e42da880c61e |
--- a/src/HOL/ex/Cartouche_Examples.thy Fri Nov 07 16:22:25 2014 +0100 +++ b/src/HOL/ex/Cartouche_Examples.thy Fri Nov 07 16:36:55 2014 +0100 @@ -178,7 +178,7 @@ ML {* Outer_Syntax.command @{command_spec "text_cartouche"} "" - (Parse.opt_target -- Parse.source_position Parse.cartouche >> Isar_Cmd.local_theory_markup) + (Parse.opt_target -- Parse.source_position Parse.cartouche >> Thy_Output.local_theory_markup) *} text_cartouche