src/HOL/Tools/BNF/bnf_fp_util.ML

       (binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
       BNF_Comp.absT_info list -> local_theory -> 'a) ->
     binding list -> (string * sort) list -> (string * sort) list -> (string * sort) list ->
     typ list -> BNF_Comp.comp_cache -> local_theory ->
     ((BNF_Def.bnf list * BNF_Comp.absT_info list) * BNF_Comp.comp_cache) * 'a
-  val fp_antiquote_setup: binding -> theory -> theory
 end;
 
 structure BNF_FP_Util : BNF_FP_UTIL =
 struct
 

     val timer = time (timer "FP construction in total");
   in
     (((pre_bnfs, absT_infos), comp_cache'), res)
   end;
 
-fun fp_antiquote_setup binding =
+
+(** document antiquotations **)
+
+local
+
+fun antiquote_setup binding =
   Thy_Output.antiquotation_pretty_source_embedded binding
     (Args.type_name {proper = true, strict = true})
     (fn ctxt => fn fcT_name =>
        (case Ctr_Sugar.ctr_sugar_of ctxt fcT_name of
          NONE => error ("Not a known freely generated type name: " ^ quote fcT_name)

            Pretty.block (Pretty.keyword1 (Binding.name_of binding) :: Pretty.brk 1 ::
              Syntax.pretty_typ ctxt T :: Pretty.str " =" :: Pretty.brk 1 ::
              flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_ctr) ctrs)))
          end));
 
+in
+
+val _ =
+  Theory.setup
+   (antiquote_setup \<^binding>\<open>datatype\<close> #>
+    antiquote_setup \<^binding>\<open>codatatype\<close>);
+
 end;
+
+end;