src/HOL/Tools/SMT/smt_normalize.ML
changeset 59058 a78612c67ec0
parent 58132 6dcee1f6ea65
child 59621 291934bac95e
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -171,7 +171,7 @@
     1.4      if has_all_vars vs (Thm.term_of ct) then
     1.5        (case Thm.term_of ct of
     1.6          _ $ _ =>
     1.7 -          (case pairself (minimal_pats vs) (Thm.dest_comb ct) of
     1.8 +          (case apply2 (minimal_pats vs) (Thm.dest_comb ct) of
     1.9              ([], []) => [[ct]]
    1.10            | (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss')
    1.11        | _ => [])
    1.12 @@ -189,7 +189,7 @@
    1.13    fun mk_pat ct = Thm.apply (SMT_Util.instT' ct pat) ct
    1.14  
    1.15    fun mk_clist T =
    1.16 -    pairself (Thm.cterm_of @{theory}) (SMT_Util.symb_cons_const T, SMT_Util.symb_nil_const T)
    1.17 +    apply2 (Thm.cterm_of @{theory}) (SMT_Util.symb_cons_const T, SMT_Util.symb_nil_const T)
    1.18    fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
    1.19    val mk_pat_list = mk_list (mk_clist @{typ pattern})
    1.20    val mk_mpat_list = mk_list (mk_clist @{typ "pattern symb_list"})