thy_syntax.ML

 TODO:
   move datatype / primrec stuff to pre_datatype.ML (?)
 *)
 
 (*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
 
 open ThyParse;

 
 
 
 (** 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;
 
 val primrec_decl =
   name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl;