src/ZF/Tools/inductive_package.ML

               List.app (writeln o Sign.string_of_term sign o #2) axpairs
           else ()
 
   (*add definitions of the inductive sets*)
   val thy1 = thy |> Theory.add_path big_rec_base_name
-                 |> (#1 o PureThy.add_defs_i false (map Thm.no_attributes axpairs))
+                 |> (snd o PureThy.add_defs_i false (map Thm.no_attributes axpairs))
 
 
   (*fetch fp definitions from the theory*)
   val big_rec_def::part_rec_defs =
     map (get_def thy1)