src/ZF/constructor.ML

 		   (([big_case_name], flatten_typ sign big_case_typ) :: 
 		    (big_rec_name ins rec_names, rec_styp) :: 
 		    flat (map #3 rec_specs));
 
 val con_thy = extend_theory thy (big_rec_name ^ "_Constructors")
-    ([], [], [], [], const_decs, ext) axpairs;
+    ([], [], [], [], [], const_decs, ext) axpairs;
 
 (*1st element is the case definition; others are the constructors*)
 val con_defs = map (get_axiom con_thy o #1) axpairs;
 
 (** Prove the case theorem **)