--- a/src/HOL/thy_syntax.ML Thu Jul 30 17:06:54 1998 +0200
+++ b/src/HOL/thy_syntax.ML Thu Jul 30 17:59:57 1998 +0200
@@ -188,7 +188,8 @@
fun mk_primrec_decl (names, eqns) =
";\nval (thy, " ^ (if null names then "_" else brackets (commas names)) ^
- ") = PrimrecPackage.add_primrec " ^ brackets (commas eqns) ^ " thy;\n\
+ ") = PrimrecPackage.add_primrec None " ^ brackets (commas_quote names) ^ " " ^
+ brackets (commas eqns) ^ " thy;\n\
\val thy = thy\n";
(* either names and axioms or just axioms *)