--- 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 @