changeset 55111 | 5792f5106c40 |
parent 49628 | 8262d35eff20 |
child 55114 | 0ee5c17f2207 |
--- a/src/HOL/Library/LaTeXsugar.thy Wed Jan 22 15:28:19 2014 +0100 +++ b/src/HOL/Library/LaTeXsugar.thy Wed Jan 22 16:03:11 2014 +0100 @@ -106,7 +106,7 @@ end in Thy_Output.antiquotation @{binding "const_typ"} - (Scan.lift Args.name_source) + (Scan.lift Args.name_inner_syntax) (fn {source = src, context = ctxt, ...} => fn arg => Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))