# HG changeset patch
# User blanchet
# Date 1408433951 -7200
# Node ID ca917ea6969c373ad87b30d0f1312730be459138
# Parent  08aa1e2cbec0fee020f2474f2e03bc198af53bff
reduced dependency on 'Datatype' theory and ML module

diff -r 08aa1e2cbec0 -r ca917ea6969c src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Aug 19 09:36:57 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Aug 19 09:39:11 2014 +0200
@@ -416,17 +416,6 @@
                    \in the problem.")
       else
         ()
-    val _ =
-      if mode = Normal andalso
-         exists (fn Type (@{type_name Datatype.node}, _) => true | _ => false)
-                all_Ts then
-        print_nt (K ("Warning: The problem involves directly or indirectly the \
-                     \internal type " ^ quote @{type_name Datatype.node} ^
-                     ". This type is very Nitpick-unfriendly, and its presence \
-                     \usually indicates either a failure of abstraction or a \
-                     \quirk in Nitpick."))
-      else
-        ()
     val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
     val _ =
       if verbose andalso not unique_scope then
diff -r 08aa1e2cbec0 -r ca917ea6969c src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Aug 19 09:36:57 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Aug 19 09:39:11 2014 +0200
@@ -198,7 +198,7 @@
   
 fun contains_recursive_type_under_function_types xs =
   exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
-    (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype.DtRec _) => true | _ => false)))) xs
+    (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype_Aux.DtRec _) => true | _ => false)))) xs
     
 fun instantiate_datatype (name, constprfx, sort, mk_equations, mk_T, argnames)
     config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
@@ -254,7 +254,7 @@
   let
     val cnstrs = flat (maps
       (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
-      (Symtab.dest (Datatype.get_all (Proof_Context.theory_of ctxt))))
+      (Symtab.dest (Datatype_Data.get_all (Proof_Context.theory_of ctxt))))
     fun is_constrt (Const (s, T), ts) = (case (AList.lookup (op =) cnstrs s, body_type T) of
         (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname'
       | _ => false)
@@ -537,19 +537,19 @@
   Quickcheck_Common.datatype_interpretation (@{sort exhaustive}, instantiate_exhaustive_datatype)
 
 val setup_bounded_forall_datatype_interpretation =
-  Datatype.interpretation (Quickcheck_Common.ensure_sort
+  Datatype_Data.interpretation (Quickcheck_Common.ensure_sort
     (((@{sort type}, @{sort type}), @{sort bounded_forall}),
-    (Datatype.the_descr, instantiate_bounded_forall_datatype)))
+    (Datatype_Data.the_descr, instantiate_bounded_forall_datatype)))
 
 val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
 
 val setup =
   Quickcheck_Common.datatype_interpretation (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
-(* #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+(* #> Datatype_Data.interpretation (Quickcheck_Common.ensure_sort_datatype
       (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
-  #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+  #> Datatype_Data.interpretation (Quickcheck_Common.ensure_sort_datatype
       (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
-  #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+  #> Datatype_Data.interpretation (Quickcheck_Common.ensure_sort_datatype
       (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
   #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
   #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
diff -r 08aa1e2cbec0 -r ca917ea6969c src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Aug 19 09:36:57 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Aug 19 09:39:11 2014 +0200
@@ -175,7 +175,7 @@
     
 fun contains_recursive_type_under_function_types xs =
   exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
-    (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype.DtRec _) => true | _ => false)))) xs
+    (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype_Aux.DtRec _) => true | _ => false)))) xs
 
 fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   let
diff -r 08aa1e2cbec0 -r ca917ea6969c src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Aug 19 09:36:57 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Aug 19 09:39:11 2014 +0200
@@ -23,15 +23,15 @@
   val generator_test_goal_terms :
     generator -> Proof.context -> bool -> (string * typ) list
       -> (term * term list) list -> Quickcheck.result list
-  type instantiation = Datatype.config -> Datatype.descr -> (string * sort) list
+  type instantiation = Datatype_Aux.config -> Datatype_Aux.descr -> (string * sort) list
      -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
   val ensure_sort :
     (((sort * sort) * sort) *
       ((theory -> string list -> Datatype_Aux.descr * (string * sort) list * string list
         * string * (string list * string list) * (typ list * typ list)) * instantiation))
-    -> Datatype.config -> string list -> theory -> theory
+    -> Datatype_Aux.config -> string list -> theory -> theory
   val ensure_common_sort_datatype :
-    (sort * instantiation) -> Datatype.config -> string list -> theory -> theory
+    (sort * instantiation) -> Datatype_Aux.config -> string list -> theory -> theory
   val datatype_interpretation : (sort * instantiation) -> theory -> theory
   val gen_mk_parametric_generator_expr :
    (((Proof.context -> term * term list -> term) * term) * typ)
@@ -387,7 +387,7 @@
 
 (** ensuring sort constraints **)
 
-type instantiation = Datatype.config -> Datatype.descr -> (string * sort) list
+type instantiation = Datatype_Aux.config -> Datatype_Aux.descr -> (string * sort) list
   -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
 
 fun perhaps_constrain thy insts raw_vs =
@@ -419,9 +419,9 @@
   end;
 
 fun ensure_common_sort_datatype (sort, instantiate) =
-  ensure_sort (((@{sort typerep}, @{sort term_of}), sort), (Datatype.the_descr, instantiate))
+  ensure_sort (((@{sort typerep}, @{sort term_of}), sort), (Datatype_Data.the_descr, instantiate))
 
-val datatype_interpretation = Datatype.interpretation o ensure_common_sort_datatype
+val datatype_interpretation = Datatype_Data.interpretation o ensure_common_sort_datatype
   
 (** generic parametric compilation **)
 
diff -r 08aa1e2cbec0 -r ca917ea6969c src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Aug 19 09:36:57 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Aug 19 09:39:11 2014 +0200
@@ -158,7 +158,7 @@
     | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
     | _ => raise CTERM ("no equation", [ct]))
 
-  fun get_constrs thy (Type (n, _)) = these (Datatype.get_constrs thy n)
+  fun get_constrs thy (Type (n, _)) = these (Datatype_Data.get_constrs thy n)
     | get_constrs _ _ = []
 
   fun is_constr thy (n, T) =
diff -r 08aa1e2cbec0 -r ca917ea6969c src/HOL/Tools/SMT2/smt2_normalize.ML
--- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Tue Aug 19 09:36:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Tue Aug 19 09:39:11 2014 +0200
@@ -144,7 +144,7 @@
     | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
     | _ => raise CTERM ("no equation", [ct]))
 
-  fun get_constrs thy (Type (n, _)) = these (Datatype.get_constrs thy n)
+  fun get_constrs thy (Type (n, _)) = these (Datatype_Data.get_constrs thy n)
     | get_constrs _ _ = []
 
   fun is_constr thy (n, T) =