# HG changeset patch
# User nipkow
# Date 756488325 -3600
# Node ID 4e68398cdc060457573b2ff7aead4c5cdbefbbf0
# Parent  9e41c6cec27c1eacaf728802ef8e1e33fd3962fa
added []-field to extend_theory: no type abbreviations.

diff -r 9e41c6cec27c -r 4e68398cdc06 src/ZF/constructor.ML
--- 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;
diff -r 9e41c6cec27c -r 4e68398cdc06 src/ZF/ind_syntax.ML
--- 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 *)
diff -r 9e41c6cec27c -r 4e68398cdc06 src/ZF/intr_elim.ML
--- 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;