src/HOL/thy_syntax.ML
changeset 5218 1a49756a2e68
parent 5183 89f162de39cf
child 5221 7e9f9ab61798
     1.1 --- a/src/HOL/thy_syntax.ML	Thu Jul 30 17:06:54 1998 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Thu Jul 30 17:59:57 1998 +0200
     1.3 @@ -188,7 +188,8 @@
     1.4  
     1.5  fun mk_primrec_decl (names, eqns) =
     1.6    ";\nval (thy, " ^ (if null names then "_" else brackets (commas names)) ^
     1.7 -  ") = PrimrecPackage.add_primrec " ^ brackets (commas eqns) ^ " thy;\n\
     1.8 +  ") = PrimrecPackage.add_primrec None " ^ brackets (commas_quote names) ^ " " ^
     1.9 +    brackets (commas eqns) ^ " thy;\n\
    1.10    \val thy = thy\n";
    1.11  
    1.12  (* either names and axioms or just axioms *)