# HG changeset patch
# User wenzelm
# Date 1575628580 -3600
# Node ID 30db0523f9b011ede80ebeb0b0f374ba454460c1
# Parent  e5664a75f4b5eb8532ff9a8ec3a7a791d39d6f07
misc tuning and clarification: proper check of datatype kind;

diff -r e5664a75f4b5 -r 30db0523f9b0 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Dec 06 11:12:55 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Dec 06 11:36:20 2019 +0100
@@ -986,35 +986,41 @@
 
 local
 
-fun antiquote_setup binding =
+fun antiquote_setup binding co =
   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)
-       | SOME {T = T0, ctrs = ctrs0, ...} =>
-         let
-           val freezeT = Term.map_atyps (fn TVar ((s, _), S) => TFree (s, S) | T => T);
+    ((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 = freezeT T0;
-           val ctrs = map (Term.map_types freezeT) ctrs0;
+              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));
+              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> #>
-    antiquote_setup \<^binding>\<open>codatatype\<close>);
+   (antiquote_setup \<^binding>\<open>datatype\<close> false #>
+    antiquote_setup \<^binding>\<open>codatatype\<close> true);
 
 end;