removed flatten_term and replaced add_axioms by add_axioms_i

--- a/src/ZF/constructor.ML	Thu Jul 07 19:47:34 1994 +0200
+++ b/src/ZF/constructor.ML	Mon Jul 11 13:15:05 1994 +0200
@@ -156,7 +156,7 @@
 
 val con_thy = thy
               |> add_consts const_decs
-              |> add_axioms axpairs
+              |> add_axioms_i axpairs
               |> add_thyname (big_rec_name ^ "_Constructors");
 
 (*1st element is the case definition; others are the constructors*)

--- a/src/ZF/ind_syntax.ML	Thu Jul 07 19:47:34 1994 +0200
+++ b/src/ZF/ind_syntax.ML	Mon Jul 11 13:15:05 1994 +0200
@@ -12,22 +12,19 @@
     let val {syn,...} = Sign.rep_sg sign 
     in  Pretty.str_of (Syntax.pretty_typ syn T)
     end;
-fun flatten_term sign t = Pretty.str_of (Sign.pretty_term sign t);
 
 (*Make a definition, lhs==rhs, checking that vars on lhs contain *)
-fun mk_defpair sign (lhs,rhs) = 
-  let val Const(name,_) = head_of lhs
+fun mk_defpair sign (lhs, rhs) = 
+  let val Const(name, _) = head_of lhs
       val dummy = assert (term_vars rhs subset term_vars lhs
-		       andalso
-		       term_frees rhs subset term_frees lhs
-		       andalso
-		       term_tvars rhs subset term_tvars lhs
-		       andalso
-		       term_tfrees rhs subset term_tfrees lhs)
+		          andalso
+		          term_frees rhs subset term_frees lhs
+		          andalso
+		          term_tvars rhs subset term_tvars lhs
+		          andalso
+		          term_tfrees rhs subset term_tfrees lhs)
 	          ("Extra variables on RHS in definition of " ^ name)
-  in  (name ^ "_def",
-       flatten_term sign (Logic.mk_equals (lhs,rhs)))
-  end;
+  in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
 
 fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
 

--- a/src/ZF/intr_elim.ML	Thu Jul 07 19:47:34 1994 +0200
+++ b/src/ZF/intr_elim.ML	Mon Jul 11 13:15:05 1994 +0200
@@ -209,7 +209,7 @@
 
 val thy = 
   Ind.thy
-  |> add_axioms axpairs
+  |> add_axioms_i axpairs
   |> add_thyname (big_rec_name ^ "_Inductive");
 
 val defs = map (get_axiom thy o #1) axpairs;