# HG changeset patch
# User wenzelm
# Date 901814397 -7200
# Node ID 1a49756a2e68a2f202e422554c6214b26d3277fb
# Parent  3ecd7c9523968f0290d99a071070ee14b2ecc9dd
fixed primrec;

diff -r 3ecd7c952396 -r 1a49756a2e68 src/HOL/thy_syntax.ML
--- 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 *)