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