added []-field to extend_theory: no type abbreviations.
authornipkow
Tue Dec 21 16:38:45 1993 +0100 (1993-12-21 ago)
changeset 2024e68398cdc06
parent 201 9e41c6cec27c
child 203 4a213aaca3d9
added []-field to extend_theory: no type abbreviations.
src/ZF/constructor.ML
src/ZF/ind_syntax.ML
src/ZF/intr_elim.ML
     1.1 --- a/src/ZF/constructor.ML	Tue Dec 21 16:27:36 1993 +0100
     1.2 +++ b/src/ZF/constructor.ML	Tue Dec 21 16:38:45 1993 +0100
     1.3 @@ -148,7 +148,7 @@
     1.4  		    flat (map #3 rec_specs));
     1.5  
     1.6  val con_thy = extend_theory thy (big_rec_name ^ "_Constructors")
     1.7 -    ([], [], [], [], const_decs, ext) axpairs;
     1.8 +    ([], [], [], [], [], const_decs, ext) axpairs;
     1.9  
    1.10  (*1st element is the case definition; others are the constructors*)
    1.11  val con_defs = map (get_axiom con_thy o #1) axpairs;
     2.1 --- a/src/ZF/ind_syntax.ML	Tue Dec 21 16:27:36 1993 +0100
     2.2 +++ b/src/ZF/ind_syntax.ML	Tue Dec 21 16:38:45 1993 +0100
     2.3 @@ -19,7 +19,7 @@
     2.4  fun thy addconsts const_decs = 
     2.5      extend_theory thy (space_implode "_" (flat (map #1 const_decs)) 
     2.6  		       ^ "_Theory")
     2.7 -		  ([], [], [], [], const_decs, None) [];
     2.8 +		  ([], [], [], [], [], const_decs, None) [];
     2.9  
    2.10  
    2.11  (*Make a definition, lhs==rhs, checking that vars on lhs contain *)
     3.1 --- a/src/ZF/intr_elim.ML	Tue Dec 21 16:27:36 1993 +0100
     3.2 +++ b/src/ZF/intr_elim.ML	Tue Dec 21 16:38:45 1993 +0100
     3.3 @@ -204,7 +204,7 @@
     3.4  		map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
     3.5  
     3.6  val thy = extend_theory Ind.thy (big_rec_name ^ "_Inductive")
     3.7 -    ([], [], [], [], [], None) axpairs;
     3.8 +    ([], [], [], [], [], [], None) axpairs;
     3.9  
    3.10  val defs = map (get_axiom thy o #1) axpairs;
    3.11