src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

 (*** this should be part of the datatype package ***)
 
 fun datatype_names_of_case_name thy case_name =
   map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
 
-fun make_case_distribs new_type_names descr sorts thy =
-  let
-    val case_combs = Datatype_Prop.make_case_combs new_type_names descr sorts thy "f";
+fun make_case_distribs new_type_names descr thy =
+  let
+    val case_combs = Datatype_Prop.make_case_combs new_type_names descr thy "f";
     fun make comb =
       let
         val Type ("fun", [T, T']) = fastype_of comb;
         val (Const (case_name, _), fs) = strip_comb comb
         val used = Term.add_tfree_names comb []

     map make case_combs
   end
 
 fun case_rewrites thy Tcon =
   let
-    val {descr, sorts, ...} = Datatype.the_info thy Tcon
+    val {descr, ...} = Datatype.the_info thy Tcon
   in
     map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
-      (make_case_distribs [Tcon] [descr] sorts thy)
+      (make_case_distribs [Tcon] [descr] thy)
   end
 
 fun instantiated_case_rewrites thy Tcon =
   let
     val rew_ths = case_rewrites thy Tcon