eliminated Sledgehammer's dependency on old-style datatypes

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Nov 21 21:33:34 2013 +0100
@@ -335,9 +335,7 @@
 (* Readable names for the more common symbolic functions. Do not mess with the
    table unless you know what you are doing. *)
 val const_trans_table =
-  [(@{type_name Product_Type.prod}, "prod"),
-   (@{type_name Sum_Type.sum}, "sum"),
-   (@{const_name False}, "False"),
+  [(@{const_name False}, "False"),
    (@{const_name True}, "True"),
    (@{const_name Not}, "Not"),
    (@{const_name conj}, "conj"),
@@ -2738,20 +2736,8 @@
                   syms []
   in (heading, decls) :: problem end
 
-val typ_of_dtyp = Logic.varifyT_global oo Datatype_Aux.typ_of_dtyp
-
-fun ctrs_of_datatype descr (_, (s, Ds, ctrs)) =
-  if forall (can Datatype_Aux.dest_DtTFree) Ds then
-    let val dataT = Type (s, map (typ_of_dtyp descr) Ds) in
-      SOME (map (fn (s, Ds) => (s, map (typ_of_dtyp descr) Ds ---> dataT)) ctrs)
-    end
-  else
-    NONE
-
-fun ctrss_of_descr descr = map_filter (ctrs_of_datatype descr) descr
-
-fun all_ctrss_of_datatypes thy =
-  Symtab.fold (snd #> #descr #> ctrss_of_descr #> append) (Datatype.get_all thy) []
+fun all_ctrss_of_datatypes ctxt =
+  map (map_filter (try dest_Const) o #ctrs) (Ctr_Sugar.ctr_sugars_of ctxt)
 
 val app_op_and_predicator_threshold = 45
 
@@ -2780,7 +2766,7 @@
       translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts
     val (_, sym_tab0) = sym_table_of_facts ctxt type_enc app_op_level conjs facts
     val mono = conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish
-    val ctrss = all_ctrss_of_datatypes thy
+    val ctrss = all_ctrss_of_datatypes ctxt
     fun firstorderize in_helper =
       firstorderize_fact thy ctrss type_enc
           (uncurried_aliases andalso not in_helper) completish sym_tab0

--- a/src/HOL/Tools/ATP/atp_util.ML	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Nov 21 21:33:34 2013 +0100
@@ -29,7 +29,6 @@
   val varify_type : Proof.context -> typ -> typ
   val instantiate_type : theory -> typ -> typ -> typ -> typ
   val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
-  val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
   val is_type_surely_finite : Proof.context -> typ -> bool
   val is_type_surely_infinite : Proof.context -> bool -> typ list -> typ -> bool
   val s_not : term -> term
@@ -191,24 +190,11 @@
     instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2)
   end
 
-fun typ_of_dtyp _ typ_assoc (Datatype.DtTFree a) =
-    the (AList.lookup (op =) typ_assoc (Datatype.DtTFree a))
-  | typ_of_dtyp descr typ_assoc (Datatype.DtType (s, Us)) =
-    Type (s, map (typ_of_dtyp descr typ_assoc) Us)
-  | typ_of_dtyp descr typ_assoc (Datatype.DtRec i) =
-    let val (s, ds, _) = the (AList.lookup (op =) descr i) in
-      Type (s, map (typ_of_dtyp descr typ_assoc) ds)
-    end
-
-fun datatype_constrs thy (T as Type (s, Ts)) =
-    (case Datatype.get_info thy s of
-       SOME {index, descr, ...} =>
-       let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
-         map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
-             constrs
-       end
-     | NONE => [])
-  | datatype_constrs _ _ = []
+fun free_constructors_of ctxt (Type (s, Ts)) =
+    (case Ctr_Sugar.ctr_sugar_of ctxt s of
+      SOME {ctrs, ...} => map_filter (try dest_Const o Ctr_Sugar.mk_ctr Ts) ctrs
+    | NONE => [])
+  | free_constructors_of _ _ = []
 
 (* Similar to "Nitpick_HOL.bounded_exact_card_of_type".
    0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
@@ -239,12 +225,11 @@
         | @{typ nat} => 0 (* optimization *)
         | Type ("Int.int", []) => 0 (* optimization *)
         | Type (s, _) =>
-          (case datatype_constrs thy T of
+          (case free_constructors_of ctxt T of
              constrs as _ :: _ =>
              let
                val constr_cards =
-                 map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
-                      o snd) constrs
+                 map (Integer.prod o map (aux slack (T :: avoid)) o binder_types o snd) constrs
              in
                if exists (curry (op =) 0) constr_cards then 0
                else Int.min (max, Integer.sum constr_cards)
@@ -270,10 +255,10 @@
                else
                  default_card
              | [] => default_card)
+        | TFree _ =>
           (* Very slightly unsound: Type variables are assumed not to be
              constrained to cardinality 1. (In practice, the user would most
              likely have used "unit" directly anyway.) *)
-        | TFree _ =>
           if not sound andalso default_card = 1 then 2 else default_card
         | TVar _ => default_card
   in Int.min (max, aux false [] T) end

--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Nov 21 21:33:34 2013 +0100
@@ -269,7 +269,15 @@
      | NONE => false)
   | _  => false
 
-val typ_of_dtyp = ATP_Util.typ_of_dtyp
+fun typ_of_dtyp _ typ_assoc (Datatype.DtTFree a) =
+    the (AList.lookup (op =) typ_assoc (Datatype.DtTFree a))
+  | typ_of_dtyp descr typ_assoc (Datatype.DtType (s, Us)) =
+    Type (s, map (typ_of_dtyp descr typ_assoc) Us)
+  | typ_of_dtyp descr typ_assoc (Datatype.DtRec i) =
+    let val (s, ds, _) = the (AList.lookup (op =) descr i) in
+      Type (s, map (typ_of_dtyp descr typ_assoc) ds)
+    end
+
 val varify_type = ATP_Util.varify_type
 val instantiate_type = ATP_Util.instantiate_type
 val varify_and_instantiate_type = ATP_Util.varify_and_instantiate_type