diff -r e191b400a8e0 -r f94fb13ecbb3 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Mon Nov 30 11:42:48 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon Nov 30 11:42:49 2009 +0100
@@ -243,7 +243,7 @@
       thy
       |> f (map snd dts)
       |-> (fn dtinfo => pair (map fst dts, SOME dtinfo))
-    handle DatatypeAux.Datatype_Empty name' =>
+    handle Datatype_Aux.Datatype_Empty name' =>
       let
         val name = Long_Name.base_name name';
         val dname = Name.variant used "Dummy";
@@ -398,7 +398,7 @@
         val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
           (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
         val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
-          (DatatypeAux.split_conj_thm thm');
+          (Datatype_Aux.split_conj_thm thm');
         val ([thms'], thy'') = PureThy.add_thmss
           [((Binding.qualified_name (space_implode "_"
              (Long_Name.qualify qualifier "inducts" :: vs' @ Ps @