src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
changeset 59058 a78612c67ec0
parent 58957 c9e744ea8a38
child 59498 50b60f501b05
--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -287,7 +287,7 @@
     end
 
   fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
-  fun dest ct = pairself dest_arg2 (Thm.dest_binop ct)
+  fun dest ct = apply2 dest_arg2 (Thm.dest_binop ct)
   val contrapos =
     Old_Z3_Proof_Tools.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
 in
@@ -482,7 +482,7 @@
 
   fun prove_refl (ct, _) = Thm.reflexive ct
   fun prove_comb f g cp =
-    let val ((ct1, ct2), (cu1, cu2)) = pairself Thm.dest_comb cp
+    let val ((ct1, ct2), (cu1, cu2)) = apply2 Thm.dest_comb cp
     in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end
   fun prove_arg f = prove_comb prove_refl f
 
@@ -506,7 +506,7 @@
   fun prove_distinct f = prove_arg (with_length (prove_list f))
 
   fun prove_eq exn lookup cp =
-    (case lookup (Logic.mk_equals (pairself Thm.term_of cp)) of
+    (case lookup (Logic.mk_equals (apply2 Thm.term_of cp)) of
       SOME eq => eq
     | NONE => if exn then raise MONO else prove_refl cp)