src/ZF/constructor.ML

 		    (big_rec_name ins rec_names, rec_styp, NoSyn) ::
 		    flat (map #3 rec_specs));
 
 val con_thy = thy
               |> add_consts const_decs
-              |> add_axioms axpairs
+              |> add_axioms_i axpairs
               |> add_thyname (big_rec_name ^ "_Constructors");
 
 (*1st element is the case definition; others are the constructors*)
 val con_defs = map (get_axiom con_thy o #1) axpairs;