fixed primrec;
authorwenzelm
Thu Jul 30 17:59:57 1998 +0200 (1998-07-30 ago)
changeset 52181a49756a2e68
parent 5217 3ecd7c952396
child 5219 924359415f09
fixed primrec;
src/HOL/thy_syntax.ML
     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 *)