# 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;