--- 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) =