# HG changeset patch
# User clasohm
# Date 774015964 -7200
# Node ID 08d1cce222e1be1833bddecc073715e6da68530a
# Parent  d4bf81734dfe51d583a5093e1d9a4d0d54cc2742
removed flatten_typ and replaced add_consts by add_consts_i

diff -r d4bf81734dfe -r 08d1cce222e1 src/ZF/constructor.ML
--- a/src/ZF/constructor.ML	Tue Jul 12 12:49:15 1994 +0200
+++ b/src/ZF/constructor.ML	Tue Jul 12 14:26:04 1994 +0200
@@ -67,17 +67,19 @@
       in (map mk_const names) @ (flatten_consts cs) end
   | flatten_consts [] = [];
 
+(*Parse type string of constructor*)
+fun read_typ (names, st, mfix) = (names, rdty st, mfix);
+
 (*Constructors with types and arguments*)
 fun mk_con_ty_list cons_pairs = 
-  let fun mk_con_ty (id, st, syn) =
-	  let val T = rdty st;
-	      val args = mk_frees "xa" (binder_types T);
-              val name = const_name id syn;
+  let fun mk_con_ty (id, T, syn) =
+        let val args = mk_frees "xa" (binder_types T);
+            val name = const_name id syn;
                             (* because of mixfix annotations the internal name 
                                can be different from 'id' *)
-	  in (name, T, args) end;
+	in (name, T, args) end;
 
-      fun pairtypes c = flatten_consts [c];
+      fun pairtypes c = flatten_consts [read_typ 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;
@@ -150,12 +152,12 @@
     big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists));
 
 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));
+		   (([big_case_name], big_case_typ, NoSyn) ::
+		    (big_rec_name ins rec_names, rdty rec_styp, NoSyn) ::
+		    map read_typ (flat (map #3 rec_specs)));
 
 val con_thy = thy
-              |> add_consts const_decs
+              |> add_consts_i const_decs
               |> add_axioms_i axpairs
               |> add_thyname (big_rec_name ^ "_Constructors");
 
diff -r d4bf81734dfe -r 08d1cce222e1 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Tue Jul 12 12:49:15 1994 +0200
+++ b/src/ZF/ind_syntax.ML	Tue Jul 12 14:26:04 1994 +0200
@@ -7,12 +7,6 @@
 *)
 
 
-(*SHOULD BE ABLE TO DELETE THESE!*)
-fun flatten_typ sign T = 
-    let val {syn,...} = Sign.rep_sg sign 
-    in  Pretty.str_of (Syntax.pretty_typ syn T)
-    end;
-
 (*Make a definition, lhs==rhs, checking that vars on lhs contain *)
 fun mk_defpair sign (lhs, rhs) = 
   let val Const(name, _) = head_of lhs