# HG changeset patch
# User clasohm
# Date 773925305 -7200
# Node ID 0d19ab250cc9a904357cbe976acfd91180bab782
# Parent  d4e82b3a06c90dd612f23ca7a1dad27200276fb6
removed flatten_term and replaced add_axioms by add_axioms_i

diff -r d4e82b3a06c9 -r 0d19ab250cc9 src/ZF/constructor.ML
--- 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*)
diff -r d4e82b3a06c9 -r 0d19ab250cc9 src/ZF/ind_syntax.ML
--- 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);
 
diff -r d4e82b3a06c9 -r 0d19ab250cc9 src/ZF/intr_elim.ML
--- 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;