| changeset 5222 | 3e40c6bffb87 |
| parent 5221 | 7e9f9ab61798 |
| child 5658 | 082debccf486 |
--- 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";