# HG changeset patch
# User wenzelm
# Date 1575627175 -3600
# Node ID e5664a75f4b5eb8532ff9a8ec3a7a791d39d6f07
# Parent  ec5090faf5414ff4f64b64edd00fb28f6dc86cbb
clarified modules;

diff -r ec5090faf541 -r e5664a75f4b5 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Dec 05 21:03:06 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Dec 06 11:12:55 2019 +0100
@@ -213,7 +213,6 @@
     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 =
@@ -982,7 +981,12 @@
     (((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 =>
@@ -1005,4 +1009,13 @@
              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;
diff -r ec5090faf541 -r e5664a75f4b5 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Dec 05 21:03:06 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Dec 06 11:12:55 2019 +0100
@@ -2606,6 +2606,4 @@
   Outer_Syntax.local_theory \<^command_keyword>\<open>codatatype\<close> "define coinductive datatypes"
     (parse_co_datatype_cmd Greatest_FP construct_gfp);
 
-val _ = Theory.setup (fp_antiquote_setup \<^binding>\<open>codatatype\<close>);
-
 end;
diff -r ec5090faf541 -r e5664a75f4b5 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Dec 05 21:03:06 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Fri Dec 06 11:12:55 2019 +0100
@@ -1870,6 +1870,4 @@
   Outer_Syntax.local_theory \<^command_keyword>\<open>datatype\<close> "define inductive datatypes"
     (parse_co_datatype_cmd Least_FP construct_lfp);
 
-val _ = Theory.setup (fp_antiquote_setup \<^binding>\<open>datatype\<close>);
-
 end;