# HG changeset patch
# User berghofe
# Date 901833281 -7200
# Node ID 3e40c6bffb877ba946c0c5cb1aa25c00078ad010
# Parent  7e9f9ab61798f9a7c4b8b76f6101a1ffa47e4d02
Fixed primrec.

diff -r 7e9f9ab61798 -r 3e40c6bffb87 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Thu Jul 30 22:58:05 1998 +0200
+++ b/src/HOL/thy_syntax.ML	Thu Jul 30 23:14:41 1998 +0200
@@ -188,7 +188,7 @@
 
 fun mk_primrec_decl (alt_name, (names, eqns)) =
   ";\nval (thy, " ^ (if null names then "_" else brackets (commas names)) ^
-  ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^
+  ") = PrimrecPackage.add_primrec (" ^ alt_name ^ ") " ^
     brackets (commas_quote names) ^ " " ^ brackets (commas eqns) ^ " thy;\n\
   \val thy = thy\n";