--- 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
*}
--- 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
--- 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
--- 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;