--- a/src/HOL/Nominal/nominal_inductive.ML Mon Nov 30 11:42:48 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Mon Nov 30 11:42:49 2009 +0100
@@ -247,7 +247,7 @@
end) prems);
val ind_vars =
- (DatatypeProp.indexify_names (replicate (length atomTs) "pi") ~~
+ (Datatype_Prop.indexify_names (replicate (length atomTs) "pi") ~~
map NominalAtoms.mk_permT atomTs) @ [("z", fsT)];
val ind_Ts = rev (map snd ind_vars);
@@ -647,7 +647,7 @@
val thss = map (fn atom =>
let val pi' = Free (pi, NominalAtoms.mk_permT (Type (atom, [])))
in map (fn th => zero_var_indexes (th RS mp))
- (DatatypeAux.split_conj_thm (Goal.prove ctxt' [] []
+ (Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] []
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p =>
let
val (h, ts) = strip_comb p;