--- a/datatype.ML Thu Sep 08 11:01:45 1994 +0200
+++ b/datatype.ML Sun Sep 11 10:31:17 1994 +0200
@@ -95,13 +95,13 @@
val primrec_decl =
let fun mkstrings((fname,tname),axms) =
let fun prove (name,eqn) =
- "val "^name^"= prove_goalw thy [get_def thy \""^fname^"\"] "
+ "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
- in ident -- long_id -- repeat1 (ident -- string) >> mkstrings end
+ in name -- long_id -- repeat1 (ident -- string) >> mkstrings end
end;
(*used for constructor parameters*)