# HG changeset patch
# User wenzelm
# Date 1394630606 -3600
# Node ID 564a7bee8652aa906b3a57eb69ace0ad3980c5d0
# Parent  61f319bebb7a3efce2dcb16e35b57e2f60105c3c
modernized setup;

diff -r 61f319bebb7a -r 564a7bee8652 src/Doc/Classes/Setup.thy
--- a/src/Doc/Classes/Setup.thy	Wed Mar 12 14:22:51 2014 +0100
+++ b/src/Doc/Classes/Setup.thy	Wed Mar 12 14:23:26 2014 +0100
@@ -6,7 +6,6 @@
 ML_file "../more_antiquote.ML"
 
 setup {*
-  More_Antiquote.setup #>
   Code_Target.set_default_code_width 74
 *}
 
diff -r 61f319bebb7a -r 564a7bee8652 src/Doc/Codegen/Setup.thy
--- a/src/Doc/Codegen/Setup.thy	Wed Mar 12 14:22:51 2014 +0100
+++ b/src/Doc/Codegen/Setup.thy	Wed Mar 12 14:23:26 2014 +0100
@@ -16,7 +16,6 @@
 ML_file "../more_antiquote.ML"
 
 setup {*
-  More_Antiquote.setup #>
 let
   val typ = Simple_Syntax.read_typ;
 in
diff -r 61f319bebb7a -r 564a7bee8652 src/Doc/Tutorial/Types/Setup.thy
--- a/src/Doc/Tutorial/Types/Setup.thy	Wed Mar 12 14:22:51 2014 +0100
+++ b/src/Doc/Tutorial/Types/Setup.thy	Wed Mar 12 14:23:26 2014 +0100
@@ -5,6 +5,4 @@
 ML_file "../../antiquote_setup.ML"
 ML_file "../../more_antiquote.ML"
 
-setup {* More_Antiquote.setup *}
-
 end
\ No newline at end of file
diff -r 61f319bebb7a -r 564a7bee8652 src/Doc/more_antiquote.ML
--- a/src/Doc/more_antiquote.ML	Wed Mar 12 14:22:51 2014 +0100
+++ b/src/Doc/more_antiquote.ML	Wed Mar 12 14:23:26 2014 +0100
@@ -1,15 +1,10 @@
 (*  Title:      Doc/more_antiquote.ML
     Author:     Florian Haftmann, TU Muenchen
 
-More antiquotations.
+More antiquotations (depending on Isabelle/HOL).
 *)
 
-signature MORE_ANTIQUOTE =
-sig
-  val setup: theory -> theory
-end;
-
-structure More_Antiquote : MORE_ANTIQUOTE =
+structure More_Antiquote : sig end =
 struct
 
 (* code theorem antiquotation *)
@@ -42,9 +37,9 @@
 
 in
 
-val setup =
-  Thy_Output.antiquotation @{binding code_thms} Args.term
-    (fn {source, context, ...} => pretty_code_thm source context);
+val _ =
+  Theory.setup (Thy_Output.antiquotation @{binding code_thms} Args.term
+    (fn {source, context, ...} => pretty_code_thm source context));
 
 end;