diff -r c480add17d52 -r 4d0545e93c0d thy_syntax.ML
--- 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;