Fixed primrec.
authorberghofe
Thu Jul 30 23:14:41 1998 +0200 (1998-07-30)
changeset 52223e40c6bffb87
parent 5221 7e9f9ab61798
child 5223 4cb05273f764
Fixed primrec.
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Thu Jul 30 22:58:05 1998 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Thu Jul 30 23:14:41 1998 +0200
     1.3 @@ -188,7 +188,7 @@
     1.4  
     1.5  fun mk_primrec_decl (alt_name, (names, eqns)) =
     1.6    ";\nval (thy, " ^ (if null names then "_" else brackets (commas names)) ^
     1.7 -  ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^
     1.8 +  ") = PrimrecPackage.add_primrec (" ^ alt_name ^ ") " ^
     1.9      brackets (commas_quote names) ^ " " ^ brackets (commas eqns) ^ " thy;\n\
    1.10    \val thy = thy\n";
    1.11