src/HOL/Tools/SMT/smt_normalize.ML

     (case Thm.term_of ct of
       Const (@{const_name HOL.eq}, _) $ _ $ _ => Thm.dest_binop ct
     | @{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) =
     let fun match (m, U) = m = n andalso Sign.typ_instance thy (T, U)
     in can (the o find_first match o get_constrs thy o Term.body_type) T end