# 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;