--- a/src/HOL/Library/LaTeXsugar.thy Fri Sep 28 08:09:28 2012 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy Fri Sep 28 08:39:48 2012 +0200
@@ -97,5 +97,21 @@
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
"_asm" :: "prop \<Rightarrow> asms" ("_")
+setup{*
+ let
+ fun pretty ctxt c =
+ let val tc = Proof_Context.read_const_proper ctxt false c
+ in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
+ Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
+ end
+ in
+ Thy_Output.antiquotation @{binding "const_typ"}
+ (Scan.lift Args.name_source)
+ (fn {source = src, context = ctxt, ...} => fn arg =>
+ Thy_Output.output ctxt
+ (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
+ end;
+*}
+
end
(*>*)
\ No newline at end of file