src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

     val T = fastype_of t
   in
     case T of
       TFree _ => NONE
     | Type (Tcon, _) =>
-      (case Datatype_Data.get_constrs (Proof_Context.theory_of ctxt) Tcon of
+      (case Datatype.get_constrs (Proof_Context.theory_of ctxt) Tcon of
         NONE => NONE
       | SOME cs =>
         (case strip_comb t of
           (Var _, []) => NONE
         | (Free _, []) => NONE