changeset 55114 | 0ee5c17f2207 |
parent 55077 | 4cf280104b85 |
parent 55111 | 5792f5106c40 |
child 55954 | a29aefc88c8d |
--- a/src/HOL/Library/LaTeXsugar.thy Wed Jan 22 10:13:40 2014 +0100 +++ b/src/HOL/Library/LaTeXsugar.thy Wed Jan 22 17:14:27 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]))