Fixed primrec.
authorberghofe
Thu Jul 30 22:58:05 1998 +0200 (1998-07-30)
changeset 52217e9f9ab61798
parent 5220 07f80f447b27
child 5222 3e40c6bffb87
Fixed primrec.
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Thu Jul 30 19:18:50 1998 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Thu Jul 30 22:58:05 1998 +0200
     1.3 @@ -186,16 +186,16 @@
     1.4  
     1.5  (** primrec **)
     1.6  
     1.7 -fun mk_primrec_decl (names, eqns) =
     1.8 +fun mk_primrec_decl (alt_name, (names, eqns)) =
     1.9    ";\nval (thy, " ^ (if null names then "_" else brackets (commas names)) ^
    1.10 -  ") = PrimrecPackage.add_primrec None " ^ brackets (commas_quote names) ^ " " ^
    1.11 -    brackets (commas eqns) ^ " thy;\n\
    1.12 +  ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^
    1.13 +    brackets (commas_quote names) ^ " " ^ brackets (commas eqns) ^ " thy;\n\
    1.14    \val thy = thy\n";
    1.15  
    1.16  (* either names and axioms or just axioms *)
    1.17 -val primrec_decl =
    1.18 -  (repeat1 (ident -- string) >> (mk_primrec_decl o ListPair.unzip)) ||
    1.19 -  (repeat1 string >> (mk_primrec_decl o (pair [])));
    1.20 +val primrec_decl = (optional ("(" $$-- name --$$ ")" >> (cat "Some")) "None" --
    1.21 +  ((repeat1 (ident -- string) >> ListPair.unzip) ||
    1.22 +   (repeat1 string >> (pair [])))) >> mk_primrec_decl;
    1.23  
    1.24  
    1.25  (** rec: interface to Slind's TFL **)