equal
deleted
inserted
replaced
616 local |
616 local |
617 val forall = |
617 val forall = |
618 SMT_Utils.mk_const_pat @{theory} @{const_name all} |
618 SMT_Utils.mk_const_pat @{theory} @{const_name all} |
619 (SMT_Utils.destT1 o SMT_Utils.destT1) |
619 (SMT_Utils.destT1 o SMT_Utils.destT1) |
620 fun mk_forall cv ct = |
620 fun mk_forall cv ct = |
621 Thm.capply (SMT_Utils.instT' cv forall) (Thm.cabs cv ct) |
621 Thm.apply (SMT_Utils.instT' cv forall) (Thm.lambda cv ct) |
622 |
622 |
623 fun get_vars f mk pred ctxt t = |
623 fun get_vars f mk pred ctxt t = |
624 Term.fold_aterms f t [] |
624 Term.fold_aterms f t [] |
625 |> map_filter (fn v => |
625 |> map_filter (fn v => |
626 if pred v then SOME (SMT_Utils.certify ctxt (mk v)) else NONE) |
626 if pred v then SOME (SMT_Utils.certify ctxt (mk v)) else NONE) |