src/HOL/Library/Old_SMT/old_z3_proof_methods.ML
changeset 59058 a78612c67ec0
parent 58957 c9e744ea8a38
child 59498 50b60f501b05
--- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -115,7 +115,7 @@
 fun prove_inj_eq ctxt ct =
   let
     val (lhs, rhs) =
-      pairself Old_SMT_Utils.mk_cprop (Thm.dest_binop (Old_SMT_Utils.dest_cprop ct))
+      apply2 Old_SMT_Utils.mk_cprop (Thm.dest_binop (Old_SMT_Utils.dest_cprop ct))
     val lhs_thm = Thm.implies_intr rhs (prove_lhs ctxt rhs lhs)
     val rhs_thm =
       Thm.implies_intr lhs (prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs)
@@ -126,7 +126,7 @@
 val swap_disj_thm = mk_meta_eq @{thm disj_commute}
 
 fun swap_conv dest eq =
-  Old_SMT_Utils.if_true_conv ((op <) o pairself Term.size_of_term o dest)
+  Old_SMT_Utils.if_true_conv ((op <) o apply2 Term.size_of_term o dest)
     (Conv.rewr_conv eq)
 
 val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm