82 val args = argsx @ args0 |
82 val args = argsx @ args0 |
83 val cT = extraTs ---> Ts ---> T |
83 val cT = extraTs ---> Ts ---> T |
84 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) |
84 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) |
85 (*Forms a lambda-abstraction over the formal parameters*) |
85 (*Forms a lambda-abstraction over the formal parameters*) |
86 val (c, thy') = |
86 val (c, thy') = |
87 Sign.declare_const [Markup.property_internal] ((Name.binding cname, cT), NoSyn) thy |
87 Sign.declare_const [Markup.property_internal] ((Binding.name cname, cT), NoSyn) thy |
88 val cdef = cname ^ "_def" |
88 val cdef = cname ^ "_def" |
89 val thy'' = Theory.add_defs_i true false [(cdef, Logic.mk_equals (c, rhs))] thy' |
89 val thy'' = Theory.add_defs_i true false [(cdef, Logic.mk_equals (c, rhs))] thy' |
90 val ax = Thm.axiom thy'' (Sign.full_name thy'' cdef) |
90 val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef) |
91 in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end |
91 in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end |
92 | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx = |
92 | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx = |
93 (*Universal quant: insert a free variable into body and continue*) |
93 (*Universal quant: insert a free variable into body and continue*) |
94 let val fname = Name.variant (add_term_names (p, [])) a |
94 let val fname = Name.variant (add_term_names (p, [])) a |
95 in dec_sko (subst_bound (Free (fname, T), p)) thx end |
95 in dec_sko (subst_bound (Free (fname, T), p)) thx end |