src/HOL/Tools/old_primrec.ML
changeset 33968 f94fb13ecbb3
parent 33963 977b94b64905
child 34952 bd7e347eb768
--- a/src/HOL/Tools/old_primrec.ML	Mon Nov 30 11:42:48 2009 +0100
+++ b/src/HOL/Tools/old_primrec.ML	Mon Nov 30 11:42:49 2009 +0100
@@ -21,7 +21,7 @@
 structure OldPrimrec : OLD_PRIMREC =
 struct
 
-open DatatypeAux;
+open Datatype_Aux;
 
 exception RecError of string;