# HG changeset patch
# User wenzelm
# Date 1236617703 -3600
# Node ID 9fe4bbb90297c96f3fab9958c24e4d6113086bc5
# Parent  d930432adb13ddcf62a6813cb94ad686ae5e07a1
adapted to simplified ThyOutput.antiquotation interface;
fixed theory name;

diff -r d930432adb13 -r 9fe4bbb90297 src/HOL/Docs/Main_Doc.thy
--- 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{*
diff -r d930432adb13 -r 9fe4bbb90297 src/HOL/Docs/ROOT.ML
--- a/src/HOL/Docs/ROOT.ML	Mon Mar 09 17:54:27 2009 +0100
+++ b/src/HOL/Docs/ROOT.ML	Mon Mar 09 17:55:03 2009 +0100
@@ -1,2 +1,2 @@
-use_thy "MainDoc";
+use_thy "Main_Doc";