src/ZF/Tools/induct_tacs.ML

     (*associate with each constructor the datatype name and rewrites*)
     val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
 
   in
       thy |> Theory.add_path (Sign.base_name big_rec_name)
-	  |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
+	  |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
 	  |> DatatypesData.put 
 	      (Symtab.update
 	       ((big_rec_name, dt_info), DatatypesData.get thy)) 
 	  |> ConstructorsData.put
 	       (foldr Symtab.update (con_pairs, ConstructorsData.get thy))