doc-src/more_antiquote.ML
changeset 43564 9864182c6bad
parent 42361 23f352990944
     1.1 --- a/doc-src/more_antiquote.ML	Mon Jun 27 17:51:28 2011 +0200
     1.2 +++ b/doc-src/more_antiquote.ML	Mon Jun 27 22:20:49 2011 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  signature MORE_ANTIQUOTE =
     1.6  sig
     1.7 +  val setup: theory -> theory
     1.8  end;
     1.9  
    1.10  structure More_Antiquote : MORE_ANTIQUOTE =
    1.11 @@ -40,8 +41,9 @@
    1.12  
    1.13  in
    1.14  
    1.15 -val _ = Thy_Output.antiquotation "code_thms" Args.term
    1.16 -  (fn {source, context, ...} => pretty_code_thm source context);
    1.17 +val setup =
    1.18 +  Thy_Output.antiquotation @{binding code_thms} Args.term
    1.19 +    (fn {source, context, ...} => pretty_code_thm source context);
    1.20  
    1.21  end;
    1.22