--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Dec 06 11:36:20 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Dec 06 11:43:29 2019 +0100
@@ -981,47 +981,4 @@
(((pre_bnfs, absT_infos), comp_cache'), res)
end;
-
-(** document antiquotations **)
-
-local
-
-fun antiquote_setup binding co =
- Thy_Output.antiquotation_pretty_source_embedded binding
- ((Scan.ahead (Scan.lift Parse.not_eof) >> Token.pos_of) --
- Args.type_name {proper = true, strict = true})
- (fn ctxt => fn (pos, type_name) =>
- let
- fun err () =
- error ("Bad " ^ Binding.name_of binding ^ ": " ^ quote type_name ^ Position.here pos);
- in
- (case Ctr_Sugar.ctr_sugar_of ctxt type_name of
- NONE => err ()
- | SOME {kind, T = T0, ctrs = ctrs0, ...} =>
- let
- val _ = if co = (kind = Codatatype) then () else err ();
-
- val T = Logic.unvarifyT_global T0;
- val ctrs = map Logic.unvarify_global ctrs0;
-
- val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt);
- fun pretty_ctr ctr =
- Pretty.block (Pretty.breaks (Syntax.pretty_term ctxt ctr ::
- map pretty_typ_bracket (binder_types (fastype_of ctr))));
- in
- 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)
- end);
-
-in
-
-val _ =
- Theory.setup
- (antiquote_setup \<^binding>\<open>datatype\<close> false #>
- antiquote_setup \<^binding>\<open>codatatype\<close> true);
-
end;
-
-end;