168 (*Forms a lambda-abstraction over the formal parameters*) |
168 (*Forms a lambda-abstraction over the formal parameters*) |
169 val def = equals cT $ c $ rhs |
169 val def = equals cT $ c $ rhs |
170 val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy |
170 val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy |
171 (*Theory is augmented with the constant, then its def*) |
171 (*Theory is augmented with the constant, then its def*) |
172 val cdef = cname ^ "_def" |
172 val cdef = cname ^ "_def" |
173 val thy'' = Theory.add_defs_i false [(cdef, def)] thy' |
173 val thy'' = Theory.add_defs_i false false [(cdef, def)] thy' |
174 in dec_sko (subst_bound (list_comb(c,args), p)) |
174 in dec_sko (subst_bound (list_comb(c,args), p)) |
175 (n+1, (thy'', get_axiom thy'' cdef :: axs)) |
175 (n+1, (thy'', get_axiom thy'' cdef :: axs)) |
176 end |
176 end |
177 | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thx) = |
177 | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thx) = |
178 (*Universal quant: insert a free variable into body and continue*) |
178 (*Universal quant: insert a free variable into body and continue*) |