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