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