diff -r 8c1afdbea473 -r 5f9d7ed4ea0c thy_syntax.ML
--- a/thy_syntax.ML	Thu Feb 16 08:56:44 1995 +0100
+++ b/thy_syntax.ML	Sun Feb 19 15:04:39 1995 +0100
@@ -114,7 +114,7 @@
 
   (*generate string for calling add_datatype*)
   fun mk_params ((ts, tname), cons) =
-   ("val (thy, " ^ tname ^ "_add_primrec) = add_datatype\n"
+   ("val (thy, " ^ tname ^ "_add_primrec) = Datatype.add_datatype\n"
     ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
     \val thy = thy",
     "structure " ^ tname ^ " =\n\