# HG changeset patch
# User blanchet
# Date 1473073758 -7200
# Node ID ad2036bb81c674079d53ea849685045e4a08b557
# Parent  b87d9d2ca67b74c8c5e200500372731b5f998ac7
export more ML functions

diff -r b87d9d2ca67b -r ad2036bb81c6 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 05 11:35:42 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 05 13:09:18 2016 +0200
@@ -83,6 +83,16 @@
   val register_fp_sugars_raw: fp_sugar list -> local_theory -> local_theory
   val register_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory
 
+  val merge_type_args: BNF_Util.fp_kind -> ''a list * ''a list -> ''a list
+  val type_args_named_constrained_of_spec: (((('a * 'b) * 'c) * 'd) * 'e) * 'f -> 'a
+  val type_binding_of_spec: (((('a * 'b) * 'c) * 'd) * 'e) * 'f -> 'b
+  val mixfix_of_spec: ((('a * 'b) * 'c) * 'd) * 'e -> 'b
+  val mixfixed_ctr_specs_of_spec: (('a * 'b) * 'c) * 'd -> 'b
+  val map_binding_of_spec: ('a * ('b * 'c * 'd)) * 'e -> 'b
+  val rel_binding_of_spec: ('a * ('b * 'c * 'd)) * 'e -> 'c
+  val pred_binding_of_spec: ('a * ('b * 'c * 'd)) * 'e -> 'd
+  val sel_default_eqs_of_spec: 'a * 'b -> 'b
+
   val mk_parametricity_goal: Proof.context -> term list -> term -> term -> term
 
   val flat_corec_preds_predsss_gettersss: 'a list -> 'a list list list -> 'a list list list ->
@@ -468,6 +478,23 @@
 fun unflatt xsss = fold_map unflat xsss;
 fun unflattt xssss = fold_map unflatt xssss;
 
+fun cannot_merge_types fp =
+  error ("Mutually " ^ co_prefix fp ^ "recursive types must have the same type parameters");
+
+fun merge_type_arg fp T T' = if T = T' then T else cannot_merge_types fp;
+
+fun merge_type_args fp (As, As') =
+  if length As = length As' then map2 (merge_type_arg fp) As As' else cannot_merge_types fp;
+
+fun type_args_named_constrained_of_spec (((((ncAs, _), _), _), _), _) = ncAs;
+fun type_binding_of_spec (((((_, b), _), _), _), _) = b;
+fun mixfix_of_spec ((((_, mx), _), _), _) = mx;
+fun mixfixed_ctr_specs_of_spec (((_, mx_ctr_specs), _), _) = mx_ctr_specs;
+fun map_binding_of_spec ((_, (b, _, _)), _) = b;
+fun rel_binding_of_spec ((_, (_, b, _)), _) = b;
+fun pred_binding_of_spec ((_, (_, _, b)), _) = b;
+fun sel_default_eqs_of_spec (_, ts) = ts;
+
 fun ctr_sugar_kind_of_fp_kind Least_FP = Datatype
   | ctr_sugar_kind_of_fp_kind Greatest_FP = Codatatype;
 
@@ -542,23 +569,6 @@
     Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts
   | _ => replicate n false);
 
-fun cannot_merge_types fp =
-  error ("Mutually " ^ co_prefix fp ^ "recursive types must have the same type parameters");
-
-fun merge_type_arg fp T T' = if T = T' then T else cannot_merge_types fp;
-
-fun merge_type_args fp (As, As') =
-  if length As = length As' then map2 (merge_type_arg fp) As As' else cannot_merge_types fp;
-
-fun type_args_named_constrained_of_spec (((((ncAs, _), _), _), _), _) = ncAs;
-fun type_binding_of_spec (((((_, b), _), _), _), _) = b;
-fun mixfix_of_spec ((((_, mx), _), _), _) = mx;
-fun mixfixed_ctr_specs_of_spec (((_, mx_ctr_specs), _), _) = mx_ctr_specs;
-fun map_binding_of_spec ((_, (b, _, _)), _) = b;
-fun rel_binding_of_spec ((_, (_, b, _)), _) = b;
-fun pred_binding_of_spec ((_, (_, _, b)), _) = b;
-fun sel_default_eqs_of_spec (_, ts) = ts;
-
 fun add_nesting_bnf_names Us =
   let
     fun add (Type (s, Ts)) ss =
@@ -2032,8 +2042,6 @@
 fun define_co_datatypes prepare_plugins prepare_constraint prepare_typ prepare_term fp construct_fp
     ((raw_plugins, discs_sels0), specs) no_defs_lthy =
   let
-    (* TODO: sanity checks on arguments *)
-
     val plugins = prepare_plugins no_defs_lthy raw_plugins;
     val discs_sels = discs_sels0 orelse fp = Greatest_FP;