# HG changeset patch
# User wenzelm
# Date 921185782 -3600
# Node ID 6c01697e082e4c0e6817a29256d1ef3094c16f4d
# Parent  f05492a711b1f93545090f7d4b6d462c39614d15
primrec: empty attributes;

diff -r f05492a711b1 -r 6c01697e082e src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Thu Mar 11 21:55:23 1999 +0100
+++ b/src/HOL/thy_syntax.ML	Thu Mar 11 21:56:22 1999 +0100
@@ -193,9 +193,9 @@
   let
     val names = map (fn (s, _) => if s = "" then "_" else s) eqns
   in
-    ";\nval (thy, " ^ mk_list names ^
-    ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^
-      mk_list (map mk_pair (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
+    ";\nval (thy, " ^ mk_list names ^ ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^
+    mk_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) eqns) ^
+    " " ^ " thy;\n\
     \val thy = thy\n"
   end;