# HG changeset patch
# User wenzelm
# Date 1575629009 -3600
# Node ID 6e0ff949073e6a1d62628da044b80360e4716a89
# Parent  30db0523f9b011ede80ebeb0b0f374ba454460c1
clarified modules;

diff -r 30db0523f9b0 -r 6e0ff949073e src/HOL/Tools/BNF/bnf_fp_util.ML
--- 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;
diff -r 30db0523f9b0 -r 6e0ff949073e src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Dec 06 11:36:20 2019 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Dec 06 11:43:29 2019 +0100
@@ -1187,4 +1187,48 @@
        -- parse_sel_default_eqs
      >> free_constructors_cmd Unknown);
 
+
+
+(** 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_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;