src/HOL/Library/LaTeXsugar.thy
changeset 63120 629a4c5e953e
parent 62522 d32c23d29968
child 63414 beb987127d0f
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Mon May 23 20:45:10 2016 +0200
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Mon May 23 21:30:30 2016 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4        end
     1.5    in
     1.6      Thy_Output.antiquotation @{binding "const_typ"}
     1.7 -     (Scan.lift Args.name_inner_syntax)
     1.8 +     (Scan.lift Args.embedded_inner_syntax)
     1.9         (fn {source = src, context = ctxt, ...} => fn arg =>
    1.10            Thy_Output.output ctxt
    1.11              (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))