primrec: empty attributes;
authorwenzelm
Thu Mar 11 21:56:22 1999 +0100 (1999-03-11)
changeset 63566c01697e082e
parent 6355 f05492a711b1
child 6357 12448b8f92fb
primrec: empty attributes;
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Thu Mar 11 21:55:23 1999 +0100
     1.2 +++ b/src/HOL/thy_syntax.ML	Thu Mar 11 21:56:22 1999 +0100
     1.3 @@ -193,9 +193,9 @@
     1.4    let
     1.5      val names = map (fn (s, _) => if s = "" then "_" else s) eqns
     1.6    in
     1.7 -    ";\nval (thy, " ^ mk_list names ^
     1.8 -    ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^
     1.9 -      mk_list (map mk_pair (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
    1.10 +    ";\nval (thy, " ^ mk_list names ^ ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^
    1.11 +    mk_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) eqns) ^
    1.12 +    " " ^ " thy;\n\
    1.13      \val thy = thy\n"
    1.14    end;
    1.15