changeset 63120 | 629a4c5e953e |
parent 56451 | 856492b0f755 |
child 63935 | aa1fe1103ab8 |
--- a/src/Doc/Prog_Prove/LaTeXsugar.thy Mon May 23 20:45:10 2016 +0200 +++ b/src/Doc/Prog_Prove/LaTeXsugar.thy Mon May 23 21:30:30 2016 +0200 @@ -52,7 +52,7 @@ end in Thy_Output.antiquotation @{binding "const_typ"} - (Scan.lift Args.name_inner_syntax) + (Scan.lift Args.embedded_inner_syntax) (fn {source = src, context = ctxt, ...} => fn arg => Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))