--- a/thy_syntax.ML Fri Dec 09 13:39:05 1994 +0100
+++ b/thy_syntax.ML Wed Dec 14 10:32:07 1994 +0100
@@ -9,7 +9,7 @@
*)
(*the kind of distinctiveness axioms depends on number of constructors*)
-val dtK = 5; (* FIXME remove from datatype.ML, rename *)
+val dtK = 5; (* FIXME rename?, move? *)
structure ThySynData: THY_SYN_DATA =
struct
@@ -153,13 +153,12 @@
(** primrec **)
-(* FIXME add_thms_as_axms (?) *)
-
fun mk_primrec_decl ((fname, tname), axms) =
let
fun mk_prove (name, eqn) =
- "val " ^ name ^ " = prove_goalw thy [get_def thy " ^ fname ^ "] " ^ eqn ^ "\n\
- \ (fn _ => [simp_tac (HOL_ss addsimps " ^ tname ^ ".recs) 1])";
+ "val " ^ name ^ " = store_thm (" ^ quote 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 mk_prove axms)) end;