--- 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