73 |> mk_old_skolem_term_wrapper |
73 |> mk_old_skolem_term_wrapper |
74 val comb = list_comb (rhs, args) |
74 val comb = list_comb (rhs, args) |
75 in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end |
75 in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end |
76 | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss = |
76 | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss = |
77 (*Universal quant: insert a free variable into body and continue*) |
77 (*Universal quant: insert a free variable into body and continue*) |
78 let val fname = Name.variant (OldTerm.add_term_names (p,[])) a |
78 let val fname = singleton (Name.variant_list (OldTerm.add_term_names (p, []))) a |
79 in dec_sko (subst_bound (Free(fname,T), p)) rhss end |
79 in dec_sko (subst_bound (Free(fname,T), p)) rhss end |
80 | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q |
80 | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q |
81 | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q |
81 | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q |
82 | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss |
82 | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss |
83 | dec_sko _ rhss = rhss |
83 | dec_sko _ rhss = rhss |