src/ZF/Tools/inductive_package.ML

   val dummy = if !Ind_Syntax.trace then
               writeln (cat_lines (map (Syntax.string_of_term ctxt0 o #2) axpairs))
           else ()
 
   (*add definitions of the inductive sets*)
-  val (_, thy1) =
+  val thy1 =
     thy0
     |> Sign.add_path big_rec_base_name
-    |> Global_Theory.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs);
+    |> fold (snd oo Global_Theory.add_def o apfst Binding.name) axpairs;
 
 
   (*fetch fp definitions from the theory*)
   val big_rec_def::part_rec_defs =
     map (Misc_Legacy.get_def thy1)