doc-src/Main/Docs/Main_Doc.thy
changeset 37216 3165bc303f66
parent 35805 1c4a8d3b26d2
child 38323 dc2a61b98bab
--- a/doc-src/Main/Docs/Main_Doc.thy	Mon May 31 19:36:13 2010 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy	Mon May 31 21:06:57 2010 +0200
@@ -9,10 +9,10 @@
    else error "term_type_only: type mismatch";
    Syntax.pretty_typ ctxt T)
 
-val _ = ThyOutput.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
+val _ = Thy_Output.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]));
+    Thy_Output.output
+      (Thy_Output.maybe_pretty_source (pretty_term_type_only context) source [arg]));
 *}
 (*>*)
 text{*