--- a/src/HOL/Nominal/nominal_atoms.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Mon Sep 01 16:17:46 2014 +0200
@@ -100,9 +100,9 @@
val (_,thy1) =
fold_map (fn ak => fn thy =>
let val dt = ((Binding.name ak, [], NoSyn), [(Binding.name ak, [@{typ nat}], NoSyn)])
- val (dt_names, thy1) = Datatype.add_datatype Datatype.default_config [dt] thy;
+ val (dt_names, thy1) = Datatype.add_datatype Datatype_Aux.default_config [dt] thy;
- val injects = maps (#inject o Datatype.the_info thy1) dt_names;
+ val injects = maps (#inject o Datatype_Data.the_info thy1) dt_names;
val ak_type = Type (Sign.intern_type thy1 ak,[])
val ak_sign = Sign.intern_const thy1 ak