--- a/src/HOL/Docs/Main_Doc.thy Mon Mar 09 17:54:27 2009 +0100
+++ b/src/HOL/Docs/Main_Doc.thy Mon Mar 09 17:55:03 2009 +0100
@@ -1,5 +1,5 @@
(*<*)
-theory MainDoc
+theory Main_Doc
imports Main
begin
@@ -9,8 +9,10 @@
else error "term_type_only: type mismatch";
Syntax.pretty_typ ctxt T)
-val _ = ThyOutput.add_commands
- [("term_type_only", ThyOutput.args (Args.term -- Args.typ_abbrev) (ThyOutput.output pretty_term_type_only))];
+val _ = ThyOutput.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
+ (fn {source, context, ...} => fn arg =>
+ ThyOutput.output
+ (ThyOutput.maybe_pretty_source (pretty_term_type_only context) source [arg]));
*}
(*>*)
text{*