src/ZF/Tools/primrec_package.ML

   let
     val Some (fname, ftype, ls, rs, con_info, eqns) = 
 	foldr (process_eqn thy) (map snd recursion_eqns, None);
     val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns) 
     val thy' = thy |> Theory.add_path (Sign.base_name (#1 def))
-                   |> Theory.add_defs_i [def]
-    val rewrites = get_axiom thy' (#1 def) ::
+                   |> (PureThy.add_defs_i o map Thm.no_attributes) [def]
+    val rewrites = get_thm thy' (#1 def) ::
 	           map mk_meta_eq (#rec_rewrites con_info)
     val char_thms = 
 	(if !Ind_Syntax.trace then	(* FIXME message / quiet_mode (!?) *)
 	     writeln ("Proving equations for primrec function " ^ fname)
 	 else ();