added []-field to extend_theory: no type abbreviations.
--- a/src/ZF/constructor.ML Tue Dec 21 16:27:36 1993 +0100
+++ b/src/ZF/constructor.ML Tue Dec 21 16:38:45 1993 +0100
@@ -148,7 +148,7 @@
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;
--- a/src/ZF/ind_syntax.ML Tue Dec 21 16:27:36 1993 +0100
+++ b/src/ZF/ind_syntax.ML Tue Dec 21 16:38:45 1993 +0100
@@ -19,7 +19,7 @@
fun thy addconsts const_decs =
extend_theory thy (space_implode "_" (flat (map #1 const_decs))
^ "_Theory")
- ([], [], [], [], const_decs, None) [];
+ ([], [], [], [], [], const_decs, None) [];
(*Make a definition, lhs==rhs, checking that vars on lhs contain *)
--- a/src/ZF/intr_elim.ML Tue Dec 21 16:27:36 1993 +0100
+++ b/src/ZF/intr_elim.ML Tue Dec 21 16:38:45 1993 +0100
@@ -204,7 +204,7 @@
map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
val thy = extend_theory Ind.thy (big_rec_name ^ "_Inductive")
- ([], [], [], [], [], None) axpairs;
+ ([], [], [], [], [], [], None) axpairs;
val defs = map (get_axiom thy o #1) axpairs;