replaced extend_theory by new add_* functions;
changed syntax of datatype declaration

--- a/src/ZF/Fin.ML	Wed Jun 29 12:13:03 1994 +0200
+++ b/src/ZF/Fin.ML	Fri Jul 01 11:03:42 1994 +0200
@@ -16,7 +16,7 @@
 *)
 
 structure Fin = Inductive_Fun
- (val thy        = Arith.thy addconsts [(["Fin"],"i=>i")]
+ (val thy        = Arith.thy |> add_consts [("Fin", "i=>i", NoSyn)]
   val rec_doms   = [("Fin","Pow(A)")]
   val sintrs     = ["0 : Fin(A)",
                     "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"]

--- a/src/ZF/List.ML	Wed Jun 29 12:13:03 1994 +0200
+++ b/src/ZF/List.ML	Fri Jul 01 11:03:42 1994 +0200
@@ -9,10 +9,9 @@
 structure List = Datatype_Fun
  (val thy        = Univ.thy
   val rec_specs  = [("list", "univ(A)",
-                      [(["Nil"],    "i"), 
-                       (["Cons"],   "[i,i]=>i")])]
+                      [(["Nil"],    "i", NoSyn), 
+                       (["Cons"],   "[i,i]=>i", NoSyn)])]
   val rec_styp   = "i=>i"
-  val ext        = None
   val sintrs     = ["Nil : list(A)",
                     "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"]
   val monos      = []

--- a/src/ZF/constructor.ML	Wed Jun 29 12:13:03 1994 +0200
+++ b/src/ZF/constructor.ML	Fri Jul 01 11:03:42 1994 +0200
@@ -22,10 +22,9 @@
 signature CONSTRUCTOR =
   sig
   val thy        : theory		(*parent theory*)
-  val rec_specs  : (string * string * (string list * string)list) list
+  val rec_specs  : (string * string * (string list * string * mixfix)list) list
                       (*recursion ops, types, domains, constructors*)
   val rec_styp	 : string		(*common type of all recursion ops*)
-  val ext        : Syntax.sext option	(*syntax extension for new theory*)
   val sintrs     : string list		(*desired introduction rules*)
   val monos      : thm list		(*monotonicity of each M operator*)
   val type_intrs : thm list		(*type-checking intro rules*)
@@ -63,15 +62,21 @@
    (fn a => "Name of recursive set not an identifier: " ^ a);
 
 (*Expands multiple constant declarations*)
-fun pairtypes (cs,st) = map (rpair st) cs;
+fun flatten_consts ((names, typ, mfix) :: cs) =
+      let fun mk_const name = (name, typ, mfix)
+      in (map mk_const names) @ (flatten_consts cs) end
+  | flatten_consts [] = [];
 
 (*Constructors with types and arguments*)
 fun mk_con_ty_list cons_pairs = 
-  let fun mk_con_ty (a,st) =
-	  let val T = rdty st
-	      val args = mk_frees "xa" (binder_types T)
-	  in  (a,T,args) end
-  in  map mk_con_ty (flat (map pairtypes cons_pairs))  end;
+  let fun mk_con_ty (a, st, syn) =
+	  let val T = rdty st;
+	      val args = mk_frees "xa" (binder_types T);
+              val name = const_name a syn; (* adds "op" to infix constructors*)
+	  in (name, T, args) end;
+
+      fun pairtypes c = flatten_consts [c];
+  in map mk_con_ty (flat (map pairtypes cons_pairs))  end;
 
 val con_ty_lists = map (mk_con_ty_list o #3) rec_specs;
 
@@ -87,8 +92,8 @@
 
 (*Make constructor definition*)
 fun mk_con_defs (kpart, con_ty_list) = 
-  let val ncon = length con_ty_list	(*number of constructors*)
-      fun mk_def ((a,T,args), kcon) =	(*kcon = index of this constructor*)
+  let val ncon = length con_ty_list	   (*number of constructors*)
+      fun mk_def ((a,T,args), kcon) = (*kcon = index of this constructor*)
 	  mk_defpair sign 
 	     (list_comb (Const(a,T), args),
 	      mk_inject npart kpart (mk_inject ncon kcon (mk_tuple args)))
@@ -107,7 +112,7 @@
 
 (*Treatment of a single constructor*)
 fun add_case ((a,T,args), (opno,cases)) =
-    if Syntax.is_identifier a 
+    if Syntax.is_identifier a
     then (opno,   
 	  (Free(case_name ^ "_" ^ a, T), args) :: cases)
     else (opno+1, 
@@ -142,13 +147,15 @@
 val axpairs =
     big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists));
 
-val const_decs = remove_mixfixes ext
-		   (([big_case_name], flatten_typ sign big_case_typ) :: 
-		    (big_rec_name ins rec_names, rec_styp) :: 
+val const_decs = flatten_consts
+		   (([big_case_name], flatten_typ sign big_case_typ, NoSyn) ::
+		    (big_rec_name ins rec_names, rec_styp, NoSyn) ::
 		    flat (map #3 rec_specs));
 
-val con_thy = extend_theory thy (big_rec_name ^ "_Constructors")
-    ([], [], [], [], [], const_decs, ext) axpairs;
+val con_thy = thy
+              |> add_consts const_decs
+              |> add_axioms axpairs
+              |> add_thyname (big_rec_name ^ "_Constructors");
 
 (*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	Wed Jun 29 12:13:03 1994 +0200
+++ b/src/ZF/ind_syntax.ML	Fri Jul 01 11:03:42 1994 +0200
@@ -14,14 +14,6 @@
     end;
 fun flatten_term sign t = Pretty.str_of (Sign.pretty_term sign t);
 
-(*Add constants to a theory*)
-infix addconsts;
-fun thy addconsts const_decs = 
-    extend_theory thy (space_implode "_" (flat (map #1 const_decs)) 
-		       ^ "_Theory")
-		  ([], [], [], [], [], const_decs, None) [];
-
-
 (*Make a definition, lhs==rhs, checking that vars on lhs contain *)
 fun mk_defpair sign (lhs,rhs) = 
   let val Const(name,_) = head_of lhs

--- a/src/ZF/intr_elim.ML	Wed Jun 29 12:13:03 1994 +0200
+++ b/src/ZF/intr_elim.ML	Fri Jul 01 11:03:42 1994 +0200
@@ -207,8 +207,10 @@
 	 | _ => rec_tms ~~		(*define the sets as Parts*)
 		map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
 
-val thy = extend_theory Ind.thy (big_rec_name ^ "_Inductive")
-    ([], [], [], [], [], [], None) axpairs;
+val thy = 
+  Ind.thy
+  |> add_axioms axpairs
+  |> add_thyname (big_rec_name ^ "_Inductive");
 
 val defs = map (get_axiom thy o #1) axpairs;