diff -r 760641387b20 -r 3226f25f88e7 datatype.ML
--- a/datatype.ML	Wed Sep 14 16:05:28 1994 +0200
+++ b/datatype.ML	Thu Sep 15 18:42:12 1994 +0200
@@ -94,13 +94,12 @@
 
 val primrec_decl =
   let fun mkstrings((fname,tname),axms) =
-    let fun prove (name,eqn) =
-      "val "^name^"= prove_goalw thy [get_def thy "^fname^"] "
-      ^ eqn ^"\n\
-       \(fn _ => [simp_tac (HOL_ss addsimps " ^ tname^".recs) 1])"
-    in ("|> " ^ tname^"_add_primrec " ^ mk_list (map snd axms)
-	, cat_lines(map prove axms))
-    end
+        let fun prove (name,eqn) =
+              "val "^name^"= prove_goalw thy [get_def thy "^fname^"] "^eqn^"\n\
+              \  (fn _ => [simp_tac (HOL_ss addsimps " ^ tname^".recs) 1])"
+            val axs = mk_list (map (fn (n,a) => mk_pair(quote n,a)) axms)
+        in ("|> " ^ tname^"_add_primrec " ^ axs, cat_lines(map prove axms))
+        end
   in name -- long_id -- repeat1 (ident -- string)  >> mkstrings end
 end;
 
@@ -523,8 +522,7 @@
 
       fun add_primrec eqns thy =
 	let val rec_comb = Const(t_rec,dummyT)
-	  val teqns = map (fn eq => snd(read_axm (sign_of thy)
-					("",eq))) eqns
+	  val teqns = map (fn neq => snd(read_axm (sign_of thy) neq)) eqns
 	  val (fname,ls,fns) = trans_recs thy cons_list teqns
 	  val rhs = 
 	    list_abs_free