83 val args = argsx @ args0 |
83 val args = argsx @ args0 |
84 val cT = extraTs ---> Ts ---> T |
84 val cT = extraTs ---> Ts ---> T |
85 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) |
85 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) |
86 (*Forms a lambda-abstraction over the formal parameters*) |
86 (*Forms a lambda-abstraction over the formal parameters*) |
87 val (c, thy') = |
87 val (c, thy') = |
88 Sign.declare_const [Markup.property_internal] ((Binding.name cname, cT), NoSyn) thy |
88 Sign.declare_const [] ((Binding.conceal (Binding.name cname), cT), NoSyn) thy |
89 val cdef = cname ^ "_def" |
89 val cdef = cname ^ "_def" |
90 val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy' |
90 val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy' |
91 val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef) |
91 val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef) |
92 in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end |
92 in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end |
93 | dec_sko (Const ("All", _) $ (Abs (a, T, p))) thx = |
93 | dec_sko (Const ("All", _) $ (Abs (a, T, p))) thx = |